Philip Zucker
@sandmouth.bsky.social
Computer Friend, Not a Bird
www.philipzucker.com
www.philipzucker.com
A toy hour clock example proof in a TLA dsl of knuckledragger. Basically combinators over `Int -> T` functions. @hillelwayne.com
October 23, 2025 at 1:52 PM
A toy hour clock example proof in a TLA dsl of knuckledragger. Basically combinators over `Int -> T` functions. @hillelwayne.com
Something I think is interesting about Knuckledragger is that the meta (python) is very different than the object language (HOL/SMTLIB).
July 23, 2025 at 10:04 PM
Something I think is interesting about Knuckledragger is that the meta (python) is very different than the object language (HOL/SMTLIB).
Starting the long haul to @sigplan-pldi.bsky.social for some early sight seeing! I’m this guy 👇. Chat me up! I’m nice! Egraphs, proof assistants, smt, or whatever you like!
June 11, 2025 at 3:36 PM
Starting the long haul to @sigplan-pldi.bsky.social for some early sight seeing! I’m this guy 👇. Chat me up! I’m nice! Egraphs, proof assistants, smt, or whatever you like!
I added knuth bendix completion as a command line program to knuckledragger
March 16, 2025 at 7:50 PM
I added knuth bendix completion as a command line program to knuckledragger
Shallow embedding intuitionistic logic in knuckledragger in the form of Kripke semantics. Kind of works! Maybe the Z3 mbqi + finite model property can save me?
March 1, 2025 at 5:02 PM
Shallow embedding intuitionistic logic in knuckledragger in the form of Kripke semantics. Kind of works! Maybe the Z3 mbqi + finite model property can save me?
Basic search functionality in knuckledragger. Not too hard given I already had a pattern matcher + python's insane self instrospection
January 24, 2025 at 5:01 PM
Basic search functionality in knuckledragger. Not too hard given I already had a pattern matcher + python's insane self instrospection
yea, you're on a list alright... OF BIG JERKS.
November 24, 2024 at 4:14 AM
yea, you're on a list alright... OF BIG JERKS.