> Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand... If you could reliable hand-proof co

> Except that the most used sorting algorithm in the world has had a real bug for years. It is very hard to prove by hand... If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. So I just stick to simple data structures and algorithms for the most part. I don't see a real need for something as complex as TimSort, when quicksort and mergesort (or even insertion sort!) are perfectly good algorithms that any high-schooler with a modicum of mathematical talent can understand. It's totally ridiculous to need an automated theorem prover to verify a sorting algorithm. > And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong... Lamport has written quite a bit about the difficulty of proofs for modern algorithms. How often were these proofs formal proofs? By which I mean that the definitions and theorem statements are just pieces of syntax in a formal system, and that the associated proofs are just calculations driven by the formal system's rules? > Even ones with Lemmas and proofs and Guy Steele's and Nir Shavit's names on them (Snark), and even ones that win "best paper" and are adopted by the industry (Chord). I would never assume an algorithm is correct just because it appears on a paper authored by famous people, or because it's widely used in industry. (You wouldn't do drugs just because famous and rich celebrities do, right?) So, unless the proof of correctness of an algorithm is so trivial that I can find the proof on my own given a couple of hints, I will demand fully formal proof. (Yes, this means that the typical CS paper, especially the typical concurrent/distributed computing paper, doesn't convince me of its thesis.) > We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. They're typically that long because they're written in a mix of natural language and mathematical notation, where the former attempts to convey intuition in order to make up for the latter failing to provide rigor. > There's no way people can do it by hand, and there's no way Haskell's type system's help is enough to help you prove it by hand. Agreed. Once we have accepted complexity in our designs, nowhere can salvation be found. So just say no to gratuitous complexity. > There's a Haskell dialect on the JVM Nice. Will check. > and a good (multithreaded!) OCaml implementation. I don't care. OCaml is an ugly language. > Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol Any examples that a non-hardware person can appreciate? (Preferably databases, but operating systems would also be okay.)