The other properties you mention are great! I'd love to verify them too. We'd be better off if those tools were widely used. But that's far from staying that what we have today isn't fantastic.
That is indeed very common, but it is neither the most important (it might be, but that requires evidence) nor is Haskell's particular blend of proof vs. burden necessarily the best. You could have said the same about Java, C#, Go or C, each with their own limited type "richness".
> We'd be better off if those tools were widely used
Formal verification tools that are able to prove many of the example I listed (or interesting-enough special cases) are far from being in wide use in the industry in absolute terms, but they are certainly in wider use than Haskell (in spite of the latter's popularity among bloggers), at least when it comes to large, complex software, which is where verification is most valuable anyway. Fujitsu have used JPF to verify a 1MLOC Java program[1], Amazon use TLA+ to verify/specify most (all?) of their AWS services (written in Java), some are quite complex[2], Esterel (or, rather, its descendants) is used by various realtime systems[3], and Intel uses TLA+ and/or internal verification tools to verify components in its processors. Each of those alone has seen more real-world "tough" industry usage than Haskell.
AFAICT, those tools are in wider use than Haskell in academia, too (aside from PL research, obviously), where they're sometimes used to verify concurrent/distributed algorithms (and in at least one famous case, prove the incorrectness of a much-lauded algorithm[4][5]).
It is, however, true that type-based verification tools (like Coq) have seen even less use than Haskell (they're basically unused in the industry) and other proof assistants are rarely used (a notable example is Isabelle, which has been used to verify the seL4 kernel, but AFAIK Isabelle isn't type-based, but, like TLA+, uses set-theory). Even in academia, use of type-based proofs is very rare (virtually nonexistent outside PL).
[1]: http://javapathfinder.sourceforge.net/events/JPF-workshop-05...
[2]: http://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-s...
[3]: http://www.esterel-technologies.com/industries/
[4]: http://www2.research.att.com/~pamela/chord-ccr.pdf
[5]: http://brooker.co.za/blog/2014/03/08/model-checking.html
I still stand by the idea that these tools should be more widely used. I also don't understand a position where they're in opposition to type theoretic approaches. Liquid Haskell extends Haskell types with an SMT silver and, frankly, most logics can import a proof with ease if you're willing to trust an external party.
It certainly has types, but I don't think it bases its proofs on type theory in the same way Coq/Agda do (but I really know nothing about it, so you may be absolutely right).
> I still stand by the idea that these tools should be more widely used.
I agree. But it's important to remember that correctness is often not boolean, and is often yet another requirement, which varies across domains and projects, and with it the effort to provide it.
> I also don't understand a position where they're in opposition to type theoretic approaches.
They're not. I simply stated that type-theoretic approaches (including Haskell) have so far gained little traction, that's all. If they one day become more popular -- I'm all for it.
The problem is that proof assistants -- be they type-based or set based -- are rarely used, and the reason is that they are notoriously hard to use, and hardly ever justify the effort. That kind of effort for correctness is only justifiable in niche applications, so those tools will always be niche tools. There's just no-way, no-how you can realistically expect large swaths of the industry to adopt them (and I'm trying to be optimistically realistic rather than a wishful-thinker). Model checkers, OTOH, are qualitatively different, and are much closer to writing tests. If the industry could be trained to write automated tests (and that has contributed greatly to the rise in software quality we've seen since the nineties, when we had a "correctness crisis"), then it can be trained to write a formal spec (a "lightweight model" as Pamela Zave calls it, or an "exhaustively-testable pseudocode" as Leslie Lamport calls it) and run a model checker. It is both more applicable, much cheaper, and much more familiar than formal proofs, and so it has a real chance at adoption. Dropping costs of computation have made it far more practical, too, for ever larger models.
As soon as you want to prove anything slightly more interesting (e.g., «this nontrivial program transformation preserves the meaning of programs», or «this implementation of serializable database transactions protects the data integrity invariants of any relational database schema»), you're completely out of luck.
But, "this implementation of serializable database transactions protects the data integrity invariants of any relational database schema" can very well be verified by model checker on a finite model for some schemas (there's little reason to believe that serializability would be affected too much by schema, other than by the graph of foreign keys), and that may be enough to gain the necessary amount of confidence in the algorithm. I can certainly see distributed-database designers using model checkers for that.
«other than by the graph of foreign keys»: That's, like, the whole point to using relational databases.
We don't have such (real) languages yet[1]. Idris is far from being production ready and or demonstrating it can be effectively used for real-workd programs. Even then, it still remains to be shown that such languages will be cheaper to use than validating the translation and still be performant enough for the purpose they're used for (and, BTW, systems that require this level of correctness usually require proofs of timing and memory use -- including stack use).
[1] There is actually one such language -- Esterel. It (and its descendants) have been used to write safety-critical software successfully. It's an incredible language, but it doesn't translate well to other domains as it's not Turing complete.
We do. Because Haskell and ML are ultimately just fancy term rewriting systems, you can do equational reasoning on their terms by hand just fine. It's even easy enough for non-[computer scientists/mathematicians] (such as yours truly) to do it casually!
Esterel can't verify a sorting algorithm (as it can't even express it), but it can verify most properties that interest developers of safety-critical control systems, including timing and memory use.
More often than not, either the monad laws are easy to verify by hand (exceptions, state, nondeterminism, etc.) or the verification can be borrowed from nLab. It's a nonproblem.
As I said in another comment, there's no general technique or tool for proving arbitrary theorems, and we have to live with that. Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
And that's exactly what can be said about the difference between Haskell's and Java's type systems. It hasn't been shown that the additional provable properties -- that are not too powerful -- do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence.
> Sometimes I use a type checker, other times I grab a pen and a piece of paper and carry out the proof by hand. Quantifier-free equational reasoning makes the latter super easy.
But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
I think there's too little agreement in this thread about what "cheaper" and "real problem" mean. I certainly find that Haskell "more cheaply" (i.e. with less mental burden) allows me, as an individual, to write programs more easily. Whether that observation scales to everyone is a very hard question to answer.
> But you said "perform your proofs in the same term language in which your program is written". If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
On the face of it, proving by manipulating Haskell expressions certainly compares favourably to proving with TLA+ and then translating into Haskell (or other language). There may, on the other hand, be additional tooling advantages around TLA+.
I think he was talking in monetary terms. And this is a useful point of view. While Haskell's beauty makes writing Haskell its own reward for some (at least me), from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business...
I think so too, but even then there are a lot of unanswered questions.
> from a practical point of view, we ought to ask ourselves «Can we actually turn Haskell's elegance into a business competitive advantage?» And, then, there's a reason why I don't run a business...
I do run a business and do believe that Haskell gives me a competitive advantage, of a sort. The interesting question is not whether this is true, but in what precise sense it is true.
Wow, nice! :-)
Yes, but you don't prove the same properties with Haskell as with TLA+ (in fact, I think that there is little overlap if any in practice). Most properties proven (well, maybe not proven but satisfactorily verified) with TLA+ (or any other sophisticated verification tool) just can't be proven in Haskell. And, again, I even prefer TLA+ to JPF (which is the tool I've had most experience with) which verifies Java bytecode directly because so far I find it more effective to verify only the core components of the algorithm. Verifying the details is usually a waste of effort (they both make the verification harder -- either harder to prove if you're doing a formal proof, or much longer to run in a model checker -- and they are easy to verify by other, informal means).
This is a little bit disingenuous, for reasons exposed below.
> do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence.
No disagreement here. I don't recall ever making any statements myself to the tone of «Haskell makes writing correct programs cheaper». But if someone else told you that, you're right - it requires empirical evidence.
> But you said "perform your proofs in the same term language in which your program is written".
And it is. Equational reasoning about Haskell programs is just using Haskell's existing reduction relation, extended with additional assumed identifications that can be used as reductions in either direction (given `a = b`, replacing either `a` for `b` or vice versa, though more often than not, only one direction is needed).
Only at the last step do we need a check that two Haskell terms are syntactically equal, which, as you say, is not doable in Haskell itself (since judgmental term equality isn't first-class), although it is trivial to do by visual inspection. The fact remains that the bulk of the work of verifying non-IO Haskell code is really just evaluating Haskell code.
> If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)?
I can't comment on what's best for Amazon's needs, since I've never worked there. And, obviously, there's a lot more software engineering talent working for Amazon than sitting in front of my keyboard.
That being said, I think the amount of effort required to evaluate Haskell[0] by hand is significantly less than the amount of effort required to translate back and forth between Java and TLA+.
And, for my needs (mainly implementing compilers and libraries of data structures and algorithms), Haskell is a significantly better language than Java (or Lisp, Python, C++, what have you). Precisely because I can reason about Haskell programs by just evaluating Haskell[0] by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic.
---
[0] Plus propositional equalities.
I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. For example, if you pick a recursive QuickSort implementation (just picked sorting because that's a classical verification example) and wanted to verify it in Haskell, you'll need to prove much more than equality at each recursive step (or unwind the entire computation and then prove equality, but that's not a very convenient proof). Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach).
Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell, and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java.
There are some interesting uses of Haskell's logic, such as session types (also possible in Java, BTW), but they are too underpowered to prove any distributed algorithm of interest (AFAICT, they are exactly as powerful as regular expressions).
What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. So it is the features of a certain algorithm which determines the language's semantics rather than an analysis of what's helpful. Good examples of the latter approach would be Java, Erlang and Clojure. (BTW, a good explanation of Java's design decision is in the first 17 minutes or so of this talk: https://www.youtube.com/watch?v=Dq2WQuWVrgQ)
That is somehow (if you squint) similar to Prolog, whose utility was determined by the quality of it search algorithms. Such approach makes for great research, but its industrial applicability is very brittle.
> Haskell is a significantly better language than Java ... Precisely because I can reason about Haskell programs by just evaluating Haskell by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic.
Even if I were to accept that premise, that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features).
EDIT:
Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; lambda substitution is a very mathematical concept).
To make this more concrete, recursion is limited assignment, and recursion combined with a continuation (or, in Haskell, a continuation monad) is imperative assignment (imperative state can be fully implemented in a pure language with continuations and recursion). So substituting across the cont monads is directly more complicated (computationally -- it requires lots of reductions) than state simulation of the very same computation.
[1]: But, forgive me, so is Java.
Now, don't get me wrong: I'm all for Clojure-style, ML-style or Rust-style immutability-by-default (each, of course, is different as they all have different tradeoffs), but that's completely separate from purity.
In those cases, one possible strategy is to take a detour via auxiliary data types, which aren't declared in the program, but are isomorphic to types that do. For example, lately I've been working quite a lot with data structures based on skew-binomial numbers (zippers, lenses and traversals for skew-binomial trees and heaps). Their usual implementation is as linked lists of increasingly weighted trees, except for the first two ones, which may have the same weight. In my proofs, however, I work with an isomorphic type with two constructors: one for the case where the weights are all strictly increasing, another for the case where the first two trees have equal weights. This is no different from performing mathematical induction on Peano naturals, but using machine integers or big integers for actually performing arithmetic operations.
> Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach).
Most algorithms that interest me are data transformations - some sequential, some parallel, but almost never concurrent. And, even in those few cases where the interleaving of concurrent computations actually matters to me (e.g., implementing serializable transaction support in a RDBMS that works for any valid schema), I highly doubt that the tools you mention have anything useful to offer, although I would love to be wrong here.
> Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java.
For things like protocol verification, I'll take a substructural type system, like those of Rust and ATS, where non-forgeable, non-duplicable tokens are used to reify the states and transitions concurrent computations may undergo. This still offers an easier, more integrated workflow than translating between two different languages.
> What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience.
My analysis of what strength is needed is very simple: If the computer can do something perfectly, let it do it. If the computer can't do it perfectly, I'll do it myself. I have no taste for automated mistakes that have to be manually rolled back, such as program analyses whose results I can't fully trust. HM-style (or, more generally, ML^F-style) type reconstruction just happens to be something that a computer can do perfectly.
> Even if I were to accept that premise, [that equational reasoning about Haskell programs is just normal Haskell term reduction]
What part is hard to accept?
> that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]).
Yep, only some aspects. Exactly the ones I happen to need to write correct programs - and prove them so.
> A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions.
Perhaps I'm just too noob, but I'm really happy that I don't need to care about tuning the behavior of a managed language's runtime system. It's too much of a black art for me to want to have anything to do with it. If performance ever becomes that much of a problem, I'll just call Rust or C++.
> But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features).
I find my productivity when using Java even lower than when using C++, which is a really impressive achievement, considering that C++ is such an unproductive language. C++ supports (to a limited extent) and encourages (to an even more limited extent) a programming style where variables actually stand for legitimate values inhabiting your problem domain (varying between assignments or member function calls, of course). These values can be manipulated using equational reasoning. In Java, every non-primitively-typed variable stands for an object reference, which is effectively a reification of the time and circumstances in which the object was created, and most certainly not something I care about. So, when it comes to actually producing proofs of correctness of Java programs, I need to jump this additional layer of indirection between variables and the values I care about. Back and forth. Over and over.
> Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine.
Of course term rewriting is computation - if it weren't, it would be useless as a theoretical basis for programming languages! But «equivalent in raw power» doesn't imply «equally convenient to use». Models of computation based on term rewriting happen to be easy to reason about in a compartmentalized, divide-and-conquer manner than Turing machines.
> So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers).
I've burned way too much time in debugger sessions that could've been usefully spent doing anything else, like writing programs that don't need to be debugged, or simply enjoying life. I don't think the value I got from them justifies the cost of opportunity. Never did a debugger session give me full confidence that the program I've written is correct. Even worse, debugger sessions seldom told me where exactly my program (as in, the code, not the running process) is wrong.
> I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time;
Speak for yourself.
> lambda substitution is a very mathematical concept).
What do you mean by «lambda substitution»? A bound variable (by any binder, such as lambda, mu, forall and exists) cannot be substituted - you need to extract the term under the binder first. If you mean «variable substitution», yes, of course it's a mathematical concept.
If you're interested in formal proofs, I suggest you read the discussion Should Your Specification Language Be Typed?[1] by Leslie Lamport (Paxos, TLA+) and Lawrence Paulson (ML, Isabelle). It is very balanced and discusses the relative pros and cons of typed and untyped proofs for formal verification (the closest they come to making a specific recommendation is exploring pluggable optional types).
> If the computer can't do it perfectly, I'll do it myself. I have no taste for automated mistakes...
You're talking about false positives, while a better approach might be to allow false negatives (as Idris does), i.e. a program doesn't typecheck without additional proof.
Alternatively, if you want the computer to do its work automatically, why stop at a simple type-checker that runs for a few seconds? Why not let the computer run a model checker for a few hours and verify some much more interesting properties? It doesn't deductively prove correctness, but it certainly increases confidence much more than testing, and it's orders-of-magnitude easier to use than any proof assistant (the authors of the seL4 kernel spent 30 man years proving 7500LOC with a theorem prover!); it's probably as easy or easier than coming up with your auxillary types.
> What part is hard to accept?
That equational reasoning is always more convenient for people than state simulation.
> Exactly the ones I happen to need to write correct programs - and prove them so.
I do that in Java. Haskell only brings you marginally closer to the correctness of a sorting algorithm than Java does (if at all) anyway. If I need more formal verification, I use a model checker (JPF in the past, now I'm about to switch to TLA+). It feels more natural for me than using types for proofs. I've found that using a model-checker that works directly on the Java code (like JPF) is not an advantage in terms of total effort over one that uses a separate specification language, especially one that's as (relatively) simple as TLA+/+Cal. I haven't tried KeY, though (also works on Java code, but uses symbolic execution; gained some publicity recently when it found a bug in a complex sorting algorithm -- in fact, possibly the world's most used sorting algorithm).
> but I'm really happy that I don't need to care about tuning the behavior of a managed language's runtime system... If performance ever becomes that much of a problem, I'll just call Rust or C++.
That's more myth than reality. HotSpot without any tuning whatsoever performs better than pretty much all managed languages. Tuning is required if you need to really come close to C-speeds, and in those cases it still requires far less work than C. But that's a whole other discussion.
> I find my productivity when using Java even lower than when using C++
I can believe that, but I was a C++ programmer for a decade before switching (primarily) to Java -- at first quite reluctantly -- and my productivity soared. However, I wasn't talking about anecdotes or personal experience. It is a proven fact that the productivity of the industry at large jumped considerably (estimates are 2x-3x on average) when it switched from C++ to Java.
> But «equivalent in raw power» doesn't imply «equally convenient to use».
Exactly.
> Models of computation based on term rewriting happen to be easy to reason about in a compartmentalized, divide-and-conquer manner than Turing machines.
True, but no one programs Turing machines. Whether term-rewriting is more convenient than mainstream imperative or imperative-functional (i.e. Clojure, ML, Erlang) requires empirical evidence which is so far sorely lacking.
> Most algorithms that interest me are data transformations - some sequential, some parallel, but almost never concurrent.
Ah, that explains it. I mostly do concurrent/distributed algorithms (I build concurrent, distributed in-memory databases).
> I highly doubt that the tools you mention have anything useful to offer, although I would love to be wrong here.
So you'll be happy to learn that you are wrong! TLA+ and friends have been used to verify lots and lots of concurrent and distributed algorithms (as well as hardware cache-coherence protocols) like Paxos, Raft,(fixed) Chord, and many, many others. See [2] and Lamport's Checking a Multithreaded Algorithm with +CAL[3]
[1]: http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
[2]: http://brooker.co.za/blog/2014/03/08/model-checking.html
I'm not interested in «balance», because this isn't a political debate, and my formal system choices don't affect anyone but me. What I do care about is convenience: not having to translate between formal systems, ruling out as many unwanted behaviors making as little effort as possible.
And the arguments in the paper in favor of the «flexibility» of untyped systems are really arguments for sloppiness. To see why a more constructive approach is better, using an example from the article, instead of saying `i - j >= 0`, I would just say `exists k. i = j + k`. This means that the witness that `i - j >= 0`, namely, their difference `k`, can be used throughout the rest of the proof without recomputing it over and over.
> (the closest they come to making a specific recommendation is exploring pluggable optional types).
I've never found optional types worth the trouble, precisely because they run into the same issues as CircleCI has experienced with core.typed: they greatly constrain typeless exploratory programming, and bring in few of the benefits of typeful exploratory programming.
> I do that in Java. Haskell only brings you marginally closer to the correctness of a sorting algorithm than Java does (if at all) anyway.
For something like a sorting algorithm, I'd just carry out the proof by hand.
> If I need more formal verification, I use a model checker (JPF in the past, now I'm about to switch to TLA+). (...) I've found that using a model-checker that works directly on the Java code (like JPF) is not an advantage in terms of total effort over one that uses a separate specification language, especially one that's as (relatively) simple as TLA+/+Cal.
I'm not going to question your experience. But all of this still seems like a lot effort to me.
> That's more myth than reality. HotSpot without any tuning whatsoever performs better than pretty much all managed languages.
I never compared HotSpot's performance with any other managed runtime. Mostly because it never gets to the point where a performance comparison matters - I don't care how fast a runtime system is if it's too hard to write correct programs that run on it.
> Tuning is required if you need to really come close to C-speeds, and in those cases it still requires far less work than C. But that's a whole other discussion.
I never said C. I'm not willing to give up the ability to define my own abstractions in a statically verifiable and enforceable manner.
> True, but no one programs Turing machines. Whether term-rewriting is more convenient than mainstream imperative or imperative-functional (i.e. Clojure, ML, Erlang) requires empirical evidence which is so far sorely lacking.
Standard ML, with a subset of its reduction relation, is a perfectly usable term rewriting system. One just needs to be aware that, while types as collections of values are sets, types as collections of terms are just presets - not all terms are equal to themselves.
> So you'll be happy to learn that you are wrong! TLA+ and friends have been used to verify lots and lots of concurrent and distributed algorithms (as well as hardware cache-coherence protocols) like Paxos, Raft,(fixed) Chord, and many, many others. See [2] and Lamport's Checking a Multithreaded Algorithm with +CAL[3]
I've never seen a convincing demonstration of how those algorithms (or anything in the distributed computing literature) can handle concurrent data structures with interesting invariants. All I see when I read those protocols is how to synchronize a single integer or something equally meaningless.
The model checker verifies this for you whether you're "sloppy" (most mathematicians wouldn't call it sloppy; just those that work in typed logic systems) or not.
> I'd just carry out the proof by hand.
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 (see http://www.envisage-project.eu/proving-android-java-and-pyth...). And besides Lamport, Zave and many others have shown that a large number of hand-proofs of complex concurrent algorithms are very often wrong. 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). Those algorithms had proofs, but the proofs were wrong: http://brooker.co.za/blog/2014/03/08/model-checking.html
If you could reliable hand-proof complex algorithms, you wouldn't need many of these tools. Lamport has written quite a bit about the difficulty of proofs for modern algorithms.
We are talking about specs that can run to 50 pages or so, and proofs that span hundreds of pages. 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.
> But all of this still seems like a lot effort to me.
It took 30 man years to deductively prove 7500 LOC with a theorem prover! It takes a few days to spec and verify Paxos or fixed Chord.
> if it's too hard to write correct programs that run on it.
There's a Haskell dialect on the JVM and a good (multithreaded!) OCaml implementation.
> All I see when I read those protocols is how to synchronize a single integer or something equally meaningless.
That's because those are the examples that fit in a tutorial. Quite a few real specs for real systems in TLA+/Alloy/Spin are available online. Here's one for Alpha's cache-coherence protocol: http://research.microsoft.com/en-us/um/people/lamport/tla/wi...
And here are all the verification annotations used to find and fix the TimSort bug: http://www.envisage-project.eu/proving-android-java-and-pyth...
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.)
It's not ridiculous when billions of dollars pass through programs using your sorting algorithm, and any improvement can matter (and there can be big differences).
> How often were these proofs formal proofs?
Do you know what percentage of algorithms have formal proofs? About 0.
> Agreed. Once we have accepted complexity in our designs, nowhere can salvation be found. So just say no to gratuitous complexity.
I've been in this industry for 20 years now, and I started out saying this, and now I hear this from others. That is obvious. Sometimes you deal with inherently complex problems. I was in the defense industry for a long time, and air-traffic control is a complex problem.
> Any examples that a non-hardware person can appreciate?
Sure. Follow the links here: http://brooker.co.za/blog/2014/03/08/model-checking.html
Also, Amazon specified Dynamo (939 lines in TLA+) and their internal distributed lock manager (mentioned in this report, with the number of lines and the kinds of bugs found: http://glat.info/pdf/formal-methods-amazon-2014-11.pdf) but I don't think they've made the actual specs available.
There are more popular languages that are faster than Haskell, languages with better tooling, and languages that are easier to learn and faster to write and read code. Haskell's claim to fame and the justification for its learning curve is verification (both formal and informal). Therefore, I think it's reasonable to compare it with verification tools.
> Haskell's claim to fame and the justification for its learning curve is verification (both formal and informal).
I think Haskell's claim to fame is being a pure language (and maybe its laziness). I don't know what languages you had in mind, but Haskell's learning curve is usually also related to people not being familiar with functional programming as a paradigm.
How would you characterize verification, then? (and remember, most verification methods aren't proofs)
> I think Haskell's claim to fame is being a pure language
Sure, but why would you want to use a pure language? I mean, you could say that any programming paradigm is intellectually interesting, but some people seem to think that using Haskell actually has some real advantages. What are those advantages? Performance? Readability? Sure, some believe it results in more maintainable code, but I think that the most common praises are "helps to reason about code equationally" -- which is informal verification -- or "helps write more correct code faster due to the rich type-system" -- which is formal verification (BTW, I say "believe" and "claim" because unfortunately we don't yet have any significant evidence to speak with confidence regarding Haskell's benefits in large, challenging real-world software because it has hardly been used in any yet).
> Haskell's learning curve is usually also related to people not being familiar with functional programming as a paradigm.
Partly, but I was quite familiar with FP (Scheme, ML) when I started learning Haskell, and there's a very steep curve (steeper than going from Java to OCaml).
No it's not. It's an informal probabilistic statement based on induction, not formal reasoning based on deduction. Stop trolling.
Formal verification is not the same as deductive proof. Some formal methods produce "probabilistic statements based on induction".
What is it that motivates you, at the same time as introducing interesting and pertinent details to a discussion, to be so negative and condescending about other people's choice of technologies?
You are clearly very intelligent and well educated. Why do you feel the need to do this? I can't for the life of me understand where this is coming from. Do you not realise how aggravating it is for the other parties in the discussion?
You have plenty to contribute by mentioning interesting technologies like TLA+ and your threading implementation. Why do you have to dump on other people at the same time?
An easy way to both start and win an argument!
No it doesn't. Troll.
Oof, that hurts. You hit us right in our sensitive areas.
* The Constructive Semantics of Pure Esterel (1999): http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2...
Both by Gérard Berry (https://en.wikipedia.org/wiki/G%C3%A9rard_Berry)