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

Your type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence Contents 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...