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

[2]: http://brooker.co.za/blog/2014/03/08/model-checking.html

[3]: http://research.microsoft.com/pubs/64627/dcas.pdf