Hacking Python's Type System for Proof Checking
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
raisestatements in Python’s type system are akin to
admitin a traditional theorem prover.