hack-python-types. Abusing 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. (see blog post)