Why Writing Correct Software Is Hard

23 Jul 2016 … and why math (alone) won’t help us I was very happy to speak at Curry On once again. Last year, following our work with Quasar, I spoke on continuations vs. monads. This year I gave a talk about computational complexity results in software verification, a subject I became interested in while formally specifying and verifying our upcoming revamped version of Galaxy. What follows is an extended version of the talk (embedded above), containing some additional proofs and results I didn’t have time to cover, complete with footnotes, for those wishing to study the topics further. Reading time: ~45 mins. In this article, we try to understand the relationship between programs and correctness, and in particular, why writing correct…