Type checker may be wrong – Lean and the Curry-Howard correspondence

Contents

• The Curry-Howard correspondence
• How do proof assistants use the CH correspondence
  • A theorem
  • A proof of the theorem
• The type checker
  • Limitations of the type checker
  • Mathematical consequences (and proof)
  • Your type checker maybe wrong
• Conclusion

When writing code many of us have been saved time and time again by type checkers: the useful piece of software that ensures you aren’t adding a string to an integer 1 or returning a reference to a value instead of the owned value. However, while useful, and sometimes annoying, it seems that the humble type checker has limited capability beyond its noble task of saving our asses…