Top all-time · #1867
Philip Zucker
Personal blog · philipzucker.com · on HN as philzookprogrammingmath
Philip Zucker writes Hey There Buddo!, a personal blog at philipzucker.com about programming and math. Since 2017, 39 different Hacker News readers have linked it 173 times, most often “Automated Propositional Sequent Proofs in the Browser with Tau Prolog”. It is still writing: the last post was on 2026-10-16, and you can follow it by feed.
Too few sampled comments (9) to say how often HN recommends it.?
Why HN links it
HN readers link Philip Zucker's blog for posts on automated theorem proving, e-graphs, Prolog-based tools and verification, such as a browser sequent prover that renders LaTeX proof trees.
- Recommended for · 4 comments
- Calls the Tau Prolog sequent prover with LaTeX proof trees a promising approach; says combining Otten's prover with TeX output is awesome; 'Love it!'; a cool li
Summarised by Claude from a sample of 9 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
A blog about life, programming, math, logic, and physics.
Most-linked posts?
- Automated Propositional Sequent Proofs in the Browser with Tau Prolog4 people · 5 mentions · first linked 2021-02-07
- Comparing Two Verilog CPU Implementations Using EBMC3 people · 3 mentions · first linked 2025-02-11
- Copy and Micropatch: Writing Binary Patches in C with Clang Preserve_none2 people · 3 mentions · first linked 2024-03-08
- PCode2C: Steps Towards Translation Validation with Ghidra and CBMC2 people · 2 mentions · first linked 2024-01-05
- Calling Lean Functions as Python Functions2 people · 2 mentions · first linked 2026-02-05
- Refinement E-Graphs2 people · 2 mentions · first linked 2026-10-05
- Modeling TLA+ in Z3Py2 people · 2 mentions · first linked 2020-12-21
- Ghidra + CBMC = Assembly Model Checker2 people · 2 mentions · first linked 2026-10-18
- Stupid Z3Py Tricks: Verifying Sorting Networks2 people · 2 mentions · first linked 2019-12-24
- Computational Category Theory in Python I: Dictionaries for FinSet2 people · 2 mentions · first linked 2020-04-07
What Hacker News says?
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
Comment linking /souffle-egg4/
on “Ask HN: What are some cool but obscure data structures you know about?”Submitted The C bounded model checker: criminally underused as a story · 209 points
HN discussionhttp://www.philipzucker.com/ Functional programming, formal methods, category theory, physics, robotics, control I like to blog little implementations of interesting ideas and explanations. Trying to make the abstract concrete. You might like it if you like the topics I like. Me dunno.
Comment linking /
on “Ask HN: What is your blog and why should I read it?”Submitted SQL, Homomorphisms and Constraint Satisfaction Problems as a story · 153 points
HN discussionFiddling with building a theorem prover https://www.philipzucker.com/egglog/ Building a robot that places marbles into a picture https://www.philipzucker.com/marble-machine-progress/
Comment linking /marble-machine-progress/
on “Ask HN: What you up to? (Who doesn't want to be hired?)”Submitted Compiling with Constraints as a story · 126 points
HN discussionBeing into functional programming helps quite a bit I think. In particular, category theory seems to nest well and illuminate some complicated uses of polymorphism and continuation passing style transformations. Categories are also a useful abstraction/pattern for designing interfaces to libraries. It's sort of a more mathematically flavored version of dataflow style libraries like simulink or gnuradio diagrams and…
Comment linking /linear-relation-algebra-of-circuits-with-hmatrix/
on “Category Theory for Programmers (2014) [pdf]”Submitted Computational Category Theory in Python III: Monoids, Groups, and Preorders as a story · 119 points
HN discussionYou can without too much work transpile datalog to SQL. SQL does have such strong support that it is useful https://github.com/philzook58/snakelog or perhaps just do it manually https://www.philipzucker.com/tiny-sqlite-datalog/
Comment linking /tiny-sqlite-datalog/
on “The "missing" graph datatype already exists. It was invented in the '70s”Submitted Linear Algebra of Types (2019) as a story · 115 points
HN discussionI'm working on Knuckledragger, a proof assistant shallowly based upon z3py https://github.com/philzook58/knuckledragger Yesterday I proved the infinitude of primes, which I was pretty happy with. https://www.philipzucker.com/knuckle_primes/ A trivial theorem in the scheme of things, but one for which z3 certainly can't do it on it's own.
Comment linking /knuckle_primes/
on “Ask HN: What are you working on? (September 2025)”Submitted Translating My Z3 Tutorial to Coq as a story · 108 points
HN discussionThe most important thing about blogging is to just get started and make it low energy. However, I was using wordpress for ~5 years and it was rotting under my feet. It served really slow. I also feel much more secure not having my content in a somewhat difficult to decipher xml file. I feel like if you don't have your content in a relatively straightforward form like plaintext or markdown or html, you're gonna lose…
Comment linking /i-moved-my-blog-from-wordpress/
on “Blogging vs. Blog Setups”Submitted Why I think Haskell is the best general purpose language as of June 22 2019 as a story · 101 points
HN discussionNice! I'll note there is a really shallow version of naive datalog I rather like if you're willing to compromise on syntax and nonlinear variable use. edge = {(1,2), (2,3)} path = set() for i in range(10): # path(x,y) :- edge(x,y). path |= edge # path(x,z) :- edge(x,y), path(y,z). path |= {(x,z) for x,y in edge for (y1,z) in path if y == y1} Similarly it's pretty easy to hand write SQL in a style that looks similar…
Comment linking /tiny-sqlite-datalog/
on “Implementing Logic Programming”Submitted Lambda MicroEgg as a story · 84 points
HN discussionJust celebrated my 10 year anniversary https://www.philipzucker.com/ten_year_blog/ actually. It has not generated new jobs for me, but I haven't been looking really. Writing is good. It's a good way to learn more. It's good to do things and have tangible results. If you don't enjoy it on some level or feel satisfaction, there are more direct ways to seek what you want.
Comment linking /ten_year_blog/
on “Ask HN: Is maintaining a personal blog still worth it?”Submitted Don't implement unification by recursion as a story · 83 points
HN discussionThis is actually one of the reasons I've been tinkering with CBMC https://www.philipzucker.com/pcode2c/ The idea is to use Ghidra to lift a specialized C interpreter of the machine code and then compare to source or ask other questions via CBMC
Comment linking /pcode2c/
on “The C bounded model checker: criminally underused”Submitted Symbolic Execution by Overloading __bool__ as a story · 81 points
HN discussionThe 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.
Comment linking /javascript-automated-proving/
on “Formalising Mathematics: An Introduction”Submitted Knuckledragger, a Semi-Automated Python Proof Assistant as a story · 71 points
HN discussionI love MIP. It's super useful. I like to think that MIP is a framework that meets halfway between a natural modeling language and a natural solution language. The reason it's good is that the framework naturally lends itself to abusing linear programming as a subroutine, which can cut out a large amount of search state space. And you tend to find you can encode many problems without too much difficulty with just a h…
Comment linking /flappy-bird-as-a-mixed-integer-program/
on “Using mixed integer programming to assign air cargo to flights”Submitted Ordinals aren't much worse than Quaternions as a story · 62 points
HN discussionNeat! Author here. Pleasantly surprised to see this made it on here. You can find the corresponding video tutorial here https://www.youtube.com/watch?v=56IIrBZy9Rc&t=13s&ab_channel... and github repo here https://github.com/philzook58/z3_tutorial and an assortment of blog posts from which I pulled some of the material of this tutorial here https://www.philipzucker.com/ and a translation of some of this tutorial to C…
Comment linking /translating-z3-to-coq/
on “Z3 Tutorial”Submitted Making a “MiniKanren” using Z3Py as a story · 62 points
HN discussionOne of the easiest to get started on Datalog in my opinion is really clingo https://potassco.org/clingo/ , which can be pip installed and has python bindings. Answer Set Programming goes beyond datalog, but it holds datalog semantics as a sublanguage. It is unfortunate this is not well advertised. pip install clingo #! clingo edge(1,2). edge(2,3). path(X,Y) :- edge(X,Y). path(X,Z) :- edge(X,Y), path(Y,Z). Datalog ha…
Comment linking /notes/Logic/answer-set-programming/
on “Learn Datalog Today”Submitted Where are all the rewrite rules? as a story · 59 points
HN discussionIt's interesting how sometimes it feels like a topic starts showing up super often all of the sudden. It probably isn't a coincidence, since my interest and probably this post's interest is due to Tao's recent equation challenge https://teorth.github.io/equational_theories/ . I was surprised and intrigued to find Wolfram's name when I was reading background literature doing this blog post https://www.philipzucker.co…
Comment linking /cody_sheffer/
on “Who Can Understand the Proof? A Window on Formalized Mathematics”Submitted Hashing Modulo Theories as a story · 59 points
HN discussion
