> 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.
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.
> In those cases, one possible strategy is to take a detour via auxiliary data types...
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/lamport-types.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/l...
[2]: http://brooker.co.za/blog/2014/03/08/model-checking.html http://brooker.co.za/blog/2014/03/08/model-checking.html
[3]: http://research.microsoft.com/pubs/64627/dcas.pdf http://research.microsoft.com/pubs/64627/dcas.pdf