Posts
2021
-
Hacking Python's Type System for Proof Checking
Dec 5
Using Python’s type-checker (mypy) to construct a propositional, constructive logic proof checker via the Curry-Howard correspondence and the BHK interpretation of intuitionistic logic. In this system, it turns out
pass
andraise
statements in Python’s type system are akin toadmit
in a traditional theorem prover.