Type Slowly

A really interesting article from Edward Yang on the purpose of formal proof in real world software, that’s kinda related to one of my dissertation ideas. In a nutshell, Curry-Howard doesn’t guarantee the correctness of a program, as it provides a proof that the program does what it does, not that it does what it should do, and the sort of proofs we should be cultivating are tools for designing systems, and communicating their purpose. This ties in nicely with my idea of a semi-formal specification DSL that could be used in a similar way to a behaviour specification or unit test in BDD/TDD.