> finding an algorithm that does it (perhaps together with some other latency requirements) is extremely hard and it took many years to find the first one that could do it.
I agree. And correctly implementing those algorithms is much easier using a formal derivation with a mathematical tool such as the predicate calculus than it is by just eyeballing it and hoping your tests catch all errors.
> But hard problems come up all the time, especially when concurrency is involved
Predicate transformers are well suited for reasoning about nondeterminism and concurrency.
> Not if it's done formally
Program derivation with predicate transformers is done formally. It's a chain of equivalences, implications, and consequences as appropriate to the problem. The program text is literally developed as a proof, and each transformation of the code must be justified by axiom, theorem, or lemma and at the end of that derivation all properties of the specification hold. You can't possibly be claiming that no formal mathematics was done before the invention of automated checkers, because that would be both ridiculous and observably false.
> Here is the proof: X is a program, and so, also a specification,
I disagree. A specification maps to either an empty or countably infinite set of programs that satisfy it. Also all programs satisfy countably infinitely many specifications. They are not isomorphic or even dual. In this case that conflation doesn't seem to impair our understanding too much though.
> and P(X) is some property that you want to verify for X.
Right, and the task of the programmer is to write a program text that provably establishes that P(X) holds everywhere in the program state space.
> A formal derivation of a program from the specification X ∧ P(X) will, therefore, prove P(X)
Yes this is what I meant when I said you should use the same techniques to derive the program text that you would to derive any other mathematical proof.
> it's not a trick, but a basic result in the study of the hardness of program analysis
It's a trick because it's a clever way of saying write a program for which there is no known algorithm. As of now nobody is going to be able to do that regardless of their methodology. I get the impression that you mean this to be a compelling point, but I'm not grasping how I'm better off not using mathematical reasoning to derive the programs that I do know how to write.
> The claim that it's easier to derive than to prove is just mathematically false
It's not even false it's incoherent. But I didn't make that claim. Both derivation and verification are ways to prove a program satisfies a specification.
As you say, a derivation of a program that satisfies a specification is a proof. Specifically, a proof by construction. The claim is that it's considerably easier to derive a program that satisfies some property than it is to verify if an arbitrary program satisfies that property. For example say we have a specification S: "returns a product of two primes" and two programs. P1: "Return 2^82589933-1 * 2^77232917-1" and P2: "Return 2^8258993365541237147-1". The proof of the correctness of P1 is trivial because I constructed it to be so[1]. As for P2 I have no idea if it satisfies S, but I am certain that it'll be considerably harder to convince myself and others that it does than it was for P1.
> With regards to claims about informal "proofs" or "derivations" it's hard to say anything, because the problem is not well-stated.
I've made no claims of the sort.
[1] https://primes.utm.edu/largest.html