Property-based checking [1] is pretty much the paragon of proving the mathematical correctness of a program short of a) using something like SPARK and Ada, or b

Property-based checking [1] is pretty much the paragon of proving the mathematical correctness of a program short of a) using something like SPARK and Ada, or b) using Coq or Agda to formally verify, well, everything[2]. Formal verification is difficult but most of the rigorous proofs are done exclusively outside of the language in which they were written[3]. [1] https://wiki.haskell.org/Introduction_to_QuickCheck2 https://wiki.haskell.org/Introduction_to_QuickCheck2 [2] http://www.slideshare.net/jasonreich/formal-verification-of-programming-languages-2888453 http://www.slideshare.net/jasonreich/formal-verification-of-... [3] http://adam.chlipala.net/papers/ImpurePOPL10/ http://adam.chlipala.net/papers/ImpurePOPL10/ -- The field is moving too fast for me to keep up, but last I checked the theoretical comp. sci. guys were still using a methodology similar to this. I haven't read many POPL or ICFP papers in the last few years so someone who's more in touch with cutting-edge research, please jump in.