Formal Philosophy
A tutorial series about how to think in formal methods: modeling, abstraction, symbolic tools, counterexamples, and what it means to justify a claim about software.
Tutorial 1: Approximate state tracking
A deck of cards as a mental model for state, abstraction, counterexamples, and counterexample-guided synthesis.
Tutorial 2: Isomorphism
How 1-to-1, structure-preserving translations let you change languages without changing the problem.
Tutorial 3: Tau Language
Write small executable specifications by listing invariants first, then letting a solver produce behaviors that satisfy them.
Tutorial 4: World models and continuous learning
Humans use internal models to simulate and plan. When models learn online, invariants and counterexamples become the difference between adaptation and drift.
Tutorial 5: Reformulation and compression
How changing representations creates leverage, why abstraction rhymes with compression, and how neuro-symbolic gates turn model proposals into checkable evidence.
Tutorial 6: MPRD and the algorithmic CEO
How MPRD turns model proposals into policy-gated execution, which algorithm breakthroughs support the algorithmic CEO, and why this is a concrete neuro-symbolic loop.
Tutorial 7: Good software engineering and clean code
Why user outcomes are the north star in both traditional and agentic workflows, and how best-practice rails turn intent into durable quality.
Tutorial 8: Predictive reading and scrambled text
An interactive app and scoped proof framework showing how invariants, ambiguity, and context-based prediction fit together in human reading.
Tutorial 9: Prompt engineering and precision communication
Precision communication for the agentic era. Make constraints explicit, use representation changes when the direct route is intractable, and transpile controlled language into a structured spec.
Tutorial 10: Reasoning, logic, and prediction
Two competing hypotheses about whether LLMs reason. Define reasoning, explain the GOFAI versus connectionism split, and connect the debate to checkable gates and refuters.
Tutorial 11: Attacking hard problems with Church's synthesis problem
Define Church synthesis precisely, trace what is decidable, then use a decomposition-plus-invariants workflow to run systematic, falsifiable attempts against the complexity wall.
Tutorial 12: Why current LLMs are not yet AGI
A scoped argument for the conceptual gap: strong language-pattern modeling is not yet the same as stable meaning creation, concept invention, or meaning-preserving formalization.
Glossary
A short, growing vocabulary for the words we use to think clearly: state, invariant, reachability, abstraction, soundness, and more.
Make claims explicit
Formal methods starts by forcing ambiguity into the open. If you cannot state the claim, you cannot check the claim.
Search for refuters
Tools are not there to praise you. They are there to find the smallest, sharpest counterexample that breaks what you thought was “always true.”
Refine into predictability
Proving bad states unreachable is a way of narrowing the program’s possible futures. That narrowing is what predictability means, formally.