> 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.