Posts

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 and raise statements in Python’s type system are akin to admit in a traditional theorem prover.