P
Philip Zucker
philipzucker.com · Personal blog · on HN since 2017
Philip Zucker writes on egraphs, SMT solvers, theorem proving, category theory and program verification, often with code examples.
What HN saysHN links it for its work on egraphs, Datalog and automated proving, and the author himself describes it as covering these subjects.
38HN people shared it
8linked it in comments
120stories submitted
1.8Kstory points
4 months agolast shared
2017people per year2026
Most-shared posts
- 1Automated Propositional Sequent Proofs in the Browser with Tau Prolog4 people · 35 points · first shared 2021 · 3 comments on HN
- 2Comparing Two Verilog CPU Implementations Using EBMC3 people · 15 points · first shared 2025 · 1 comments on HN
- 3Computational Category Theory in Python III: Monoids, Groups, and Preorders2 people · 123 points · first shared 2020 · 56 comments on HN
- 4Linear Algebra of Types (2019)2 people · 117 points · first shared 2019 · 8 comments on HN
- 5Compositional Datalog on SQL: Relational Algebra of the Environment2 people · 50 points · first shared 2025 · 3 comments on HN
- 6Modeling TLA+ in Z3Py2 people · 34 points · first shared 2020 · 9 comments on HN
- 7Verifying Nand2Tetris Assembly with Constrained Horn Clauses (2021)2 people · 22 points · first shared 2021 · 4 comments on HN
- 8Automated Category Theory Reasoning with Metatheory.jl and Egraphs2 people · 8 points · first shared 2021 · discussion on HN
- 9A Python Frozenset Interpretation of Dependent Type Theory2 people · 7 points · first shared 2025 · discussion on HN
- 10Annihilating My Friend Will with a Python Fluid Simulation, Like the Cur He Is2 people · 5 points · first shared 2019 · discussion on HN
- 11Computational Category Theory in Python I: Dictionaries for FinSet2 people · 5 points · first shared 2020 · discussion on HN
- 12Proving a Category Theory Theorem with Rust and Egraphs2 people · 4 points · first shared 2021 · discussion on HN
- 13Copy and Micropatch: Writing Binary Patches in C with Clang Preserve_none2 people · 4 points · first shared 2024 · discussion on HN
- 14Knuckledragger: Experimenting with a Python Proof Assistant2 people · 4 points · first shared 2024 · discussion on HN
- 15Stupid Z3Py Tricks: Verifying Sorting Networks2 people · 3 points · first shared 2019 · discussion on HN
What HN people wrote when they linked it
philzook · 2026-01-14
https://www.philipzucker.com/ I blog regularly about egraphs, SMT solvers, assembly verification, theorem proving
ishmandoo · 2018-10-18
Love it!
I implemented something similar in Mathematica:
http://blog.benwiener.com/programming/art/2017/08/24/lewitt.html
My friend implemented it in Elm:
http://www.philipzucker.com/elm-eikonal-sol-lewitt/
c-cube · 2024-10-29
It's not really clear that functional style is easier/closer to proofs, tbh: https://hillelwayne.com/post/theorem-prover-showdown/ :-).
There's absolutely a constructivist form of unification, the description of a particular unification algorithm is typically a rewrite system (OP has one here: https://www.philipzucker.com/assets/traat/unify_rules.png) which qualifies as constructive imho (it builds an explicit solution, ie a substitution). But the imperative implementation of such a rewrite system can be readable too (especially if you still have pattern matching as in, say, Rust or OCaml).
I don't think there's any link to be had with the Curry Howard correspondence here. No types, no lambda calculus, nothing of the sort.
1MachineElf · 2022-08-01
I found this cool link in one of the examples: https://www.philipzucker.com/javascript-automated-proving/
superlopuh · 2022-07-22
Yes, at least these egg-based projects are usign this idea, but it looks like it's just one of the options:
https://souffle-lang.github.io/docs.html
http://www.philipzucker.com/souffle-egg4/
https://arxiv.org/pdf/2004.03082.pdf
Jtsummers · 2021-11-29
https://www.philipzucker.com/https:/www.philipzucker.com/nand2tetris-c…
Not sure what's happening, but that's the present link on HN. It should be:
https://www.philipzucker.com/nand2tetris-chc/
EDIT: Canonical link issue:
<link rel="canonical" href="https:/www.philipzucker.com/nand2tetris-chc/" />
^
There's a typo there, causing HN to rewrite it as the first link.
carapace · 2021-02-21
The only major problem (IMO) is that Lean and the others (Coq, Hol, Isabelle, Agda, Idris, etc...) are all pretty hard to read.
Check out "Automated Propositional Sequent Proofs in Your Browser with Tau Prolog" for a promising approach: https://www.philipzucker.com/javascript-automated-proving/ It's rendering LaTeX proof trees.
adsharma · 2021-07-16
Author seems to be using https://github.com/ailidani/paxi for actual implementation and proof.
I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright
The issue is that rust is a very large language and it's hard to get it right.
I have a python implementation of raft over here:
https://github.com/adsharma/raft/tree/master/raft/states
That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages.
The issue with TLA+ proofs such as:
https://github.com/fpaxos/raft.tla
is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec.
So how do we check and transpile?
* https://www.philipzucker.com/Modelling_TLA_in_z3py/
* https://github.com/adsharma/py2many