logic

Not the keyword you're looking for? See all keywords.

Building a Tiny Theorem Prover in Python Building a Tiny Theorem Prover in Python
7 min read Keywords:  theorem proving, python, type theory, formal verification, logic, curry-howard

A tiny theorem prover is just a term language, a checker, and a small trusted kernel. We build one in plain Python to make the architecture explicit.

Propositions Are Types, Proofs Are Programs Propositions Are Types, Proofs Are Programs
12 min read Keywords:  curry-howard, type theory, theorem proving, logic, formal verification

The Curry-Howard correspondence says that types and logical propositions are the same thing. Understanding why changes how you think about both programming and mathematics.