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