Tessera
Folgen

Philip Zucker

@sandmouth.bsky.social

Computer Friend, Not a Bird www.philipzucker.com

193 Posts324 Follower361 Folgt
Philip Zucker@sandmouth.bsky.social · 24h ago

A new blog post "An Intuitionistic Micro Proof Assistant" www.philipzucker.com/kd_intu/ The basics to wrap an automated theorem prover (here intuitionistic FOL nanocopi) to make an embedded interactive theorem proving system. Reading Bell's smooth infinitesimals #python

An Intuitionistic Micro Proof Assistant

I’ve been tinkering on a solver-oriented interactive proof assistant as a library called Knuckledragger https://github.com/philzook58/knuckledragger .

philipzucker.com

Philip Zucker@sandmouth.bsky.social · last wk.

"Finite Algebraic Effects as dicts and such" www.philipzucker.com/bdd_term_alg... I like making things finite. Algebraic effects as terms with keyword args / generalized arity a la Bauer. Combinators that evaluate as a python dict. Working towards effects + egraphs ? #programminglanguages

Finite Algebraic Effects as dicts and such

Algebraic effects are a style / mathematical framework for modelling mutation, search, and some other things. They are another attempt to bridge the gap between mathy looking stuff and our crass world...

philipzucker.com

Philip Zucker@sandmouth.bsky.social · 3w ago

A new blog post "Making TLA+ and x86 Kiss Via Z3Py" www.philipzucker.com/kissin_tla/ Basically, I'm type inferring on tla2tools.jar xml output to convert to z3py expressions, then using knuckledragger z3py stuff to talk to ghidra assembly semantics. Is this a useful direction?

Making TLA+ and x86 Kiss Via Z3Py

I’ve been trying my hand at translating a reasonable subset of TLA+ into z3py for the purposes of connecting specs to Verus, CBMC, and my assembly checker and also for maybe a little interactive theor...

philipzucker.com

Lawrence Paulson@lawrpaulson.bsky.social · 3w ago

Checking Equality-Saturation Merge and Extraction Certificates AF Ramos et al Equality-saturation engines maintain equalities in an e-graph and later extract a representative from an e-class. We verify an executable checker. For extraction a finite e-graph is represented as an ordered e-class DAG.

Checking Equality-Saturation Merge and Extraction Certificates

Checking Equality-Saturation Merge and Extraction Certificates in the Archive of Formal Proofs

isa-afp.org

Philip Zucker@sandmouth.bsky.social · 4w ago

A new blog post "Lifting Terms: Making Well Scoped Syntax Dumber" www.philipzucker.com/thin_term/ Basically, add a field to regular terms that says what scope you're in and which variables you use. Lifting e-graphs minus the e-graph.

Lifting Terms: Making Well Scoped Syntax Dumber

I have been writing posts about Lifting Egraphs video as an intriguing way of adding variables and scope into an egraph. But pulling back a little, I can see that the simpler thing to talk about first...

philipzucker.com

Philip Zucker@sandmouth.bsky.social · last mo.

A new blog post "A Theory of Arrays (ToA) Union Find" www.philipzucker.com/toa_unionfind/ Another non group union find inspired by semi-persistent arrays. You can support "store" annotations on edges if you swap data out of the "lattice" on the root when you reroot.

A Theory of Arrays (ToA) Union Find

One thing I’ve been discussing with Rudi, Michel and Max is union find annotations. Union find enhancements that still feel like union finds.

philipzucker.com

Philip Zucker@sandmouth.bsky.social · 2mo ago

On Monday morn I'll be giving a talk at @sigplan-pldi.bsky.social #PLDI EGRAPHS 2026 about lifting egraphs pldi26.sigplan.org/details/egra... a new twist on adding a notion of rigid alpha canonical variables to e-graphs! Pretty pumped about these ideas! Check it out!

Lifting E-Graphs: A Function Isn’t a Constant (EGRAPHS 2026) - PLDI 2026

Research in the EGRAPHS Community has recently exploded in both quantity and diversity. The data structure that powers SMT solvers is now seeing use in synthesis, optimization, and verification via eq...

pldi26.sigplan.org

Kiran@kirancodes.me · 3mo ago

Z3! You're on WATCH! Latest update to lean.py is a drop in replacement for Z3! Everyone's trying to put SMT solvers in their theorem prover, how about putting a theorem prover in your SMT solver? and here's the crazy thing: One click install, if you know Z3, you KNOW lean.py. You are not ready.

A Z3-like reasoning API for Python, backed by Lean 4 Lean 4 is a general-purpose symbolic reasoning engine. Its tactic library covers linear arithmetic (omega), congruence closure with E-matching (grind), propositional decidability (decide), and rewriting (simp), and the system is designed to be extended with new sorts, constructors, and decision procedures. Every proof is independently checked by a small trusted kernel, so the Python side never needs to trust the automation; it trusts the checker. The overhead of learning Lean’s type theory and build system has kept most of this machinery out of reach for Python programmers. lean_py.z3 wraps Lean’s tactic engine in the z3py API. Propositions are written in the familiar Int, Bool, Function, ForAll vocabulary. Under the hood, each expression compiles to a Lean 4 term, gets dispatched to the tactic engine, and the resulting proof is kernel-checked. uv pip install "lean_py @ git+https://github.com/BasisResearch/lean.py" You need elan so that lean is on your PATH. Then open Python. from lean_py.z3 import * x, y = Ints('x y') prove(Implies(And(x > 0, y > 0), x + y > 0)) # proved On the first run the library builds and caches a managed Lake project under ~/.lean_py/managed/, which takes a minute or two. Every subsequent run picks up the cache and starts instantly.
Kiran@kirancodes.me · 3mo ago

ML researchers know Python. Proof engineers know Lean. Never the two should meet.. Until now! Announcing Lean.py, effortless Lean to Python and Python to Lean bindings! - Write Lean tactics in Python - Access the Python ecosystem in Lean github.com/kiranandcode...

Kiran@kirancodes.me · 3mo ago

Craziest thing about lean.py? You can roll your own (almost) feature-parity successor to Dafny. Python programs. Lean obligations. Grind as a solver. Proof complete. Program verified. Python code. Real.

Kiran@kirancodes.me · 3mo ago

Python doesn't have a refinement type system---except now it does~ Combining algebraic effects with Lean, we can create a lightweight verification framework embedded into python~ We send the VCs off to lean, the function is verified if we can close the proof! Liquid Haskellers on suicide watch

def positive_increment(x: Annotated[int, Gt(0)]): y = x + 3 assert_refined(y, Gt(3)) # x > 0 → x + 3 > 3 ✓ z = x + 10 assert_refined(z, Gt(10)) # x > 0 → x + 10 > 10 ✓ assert verify(positive_increment) def bounded_sum(x: Annotated[int, Gt(0)], y: Annotated[int, Gt(0)]): s = x + y assert_refined(s, Gt(1)) # x > 0 ∧ y > 0 → x + y > 1 ✓ assert_refined(s, Ge(2)) # x > 0 ∧ y > 0 → x + y >= 2 ✓ assert verify(bounded_sum) def failing(x: Annotated[int, Gt(0)]): y = x + 1 assert_refined(y, Gt(10)) # x > 0 → x + 1 > 10 ✗ assert not verify(failing)
Rondo Dondo@maplant.com · 3mo ago

scheme-rs 0.2 has been released! Lots of new features but my favorite is the params system which allows you to share rust mutable variables over a scheme delimited continuation. This solves the “how do I share this mutable reference with my scripting language” problem github.com/maplant/sche...

Release Version 0.2.0 · maplant/scheme-rs

Added Added import restrictions system via allowlists (thanks @wizzeh!). Added automatically importing (rnrs (6)) if no imports are present in a scheme program. Added Basic threading library (thr...

github.com