I'm sad that in this thread and https://news.ycombinator.com/item?id=11786193, nobody is actually talking about the technical arguments at play. I've only read the EWD692 "opening salvo" but already there are interesting things to point out.
EWD1303:
> The profound significance of Dekker's solution of 1959, however, was that it showed the role that mathematical proof could play in the process of program design. Now, more than 40 years later, this role is still hardly recognized in the world of discrete designs. If mathematics is allowed to play a role at all, it is in the form of a posteriori verification, i.e. by showing by usually mechanized mathematics that the design meets its specifications; the strong guidance that correctness concerns can provide to the design process is rarely exploited. On the whole it is still "Code first, debug later" instead of "Think first, code later", which is a pity, but Computing Science cannot complain: we are free to speak, we don't have a right to be heard. And in later years Computing Science has spoken: in connection with the calculational derivation of programs —and then of mathematical proofs in general— the names of R.W. Floyd, C.A.R. Hoare, D. Gries, C.C. Morgan, A.J.M. van Gasteren and W.H.J. Feijen are the first to come to my mind.
Backus as quoted in EWD692 (Djikstra attacks this):
> One advantage of this algebra over other proof techniques is that the programmer can use his programming language as the language for deriving proofs, rather than having to state proofs in a separate logical system that merely [sic!] talks about his programs.
From a perspective of a PL person like myself, these ideals are very compatible. Without correctness by construction, there is not enough proof reuse so formality will forever be doomed for niche applications (aka computers embedded in dangerous things). Likewise after trying out intuitionistic type theory--based things (e.g. Agda) separating the program and proof langauges just seems clumsy. Overall separating programming and proof whether spatially (seperate languages) or temporally (correctness proved after the fact) is bad, and the reasons hardly depend on the dimension of separation
IIUC, Backus also talks about correctness proofs with "Von Neumann model" languages just being a lot harder to prove, a separate point from the language for the proof itself. Well, that's a huge selling point for PL research to this day, Dijkstra evidently came fully on board years later as evidenced in https://www.cs.utexas.edu/users/EWD/transcriptions/OtherDocs...:
> A fundamental reason for the preference is that functional programs are much more readily appreciated as mathematical objects than imperative ones, so that you can teach what rigorous reasoning about programs amounts to.
> separating the program and proof langauges just seems clumsy.
Lamport's TLA (which serves as the basis for TLA+) is simpler than Agda because in Agda, even though you use the same syntax for both types (i.e. propositions) and programs, they are conceptually separate, while in TLA they are the same. Both the program (well, its specification) and its properties are just logical propositions. TLA+, which is untyped (and based on TLA and ZFC) has the added advantage of being far, far (far) easier to learn than any dependently-typed language. TLA was introduced in this paper[1], which begins thus:
> Correctness of the algorithm means that the program satisfies a desired property. We propose a simpler approach in which both the algorithm and the property are specified by formulas in a single logic. Correctness of the algorithm means that the formula specifying the algorithm implies the formula specifying the property, where implies is ordinary logical implication. We are motivated not by an abstract ideal of elegance, but by the practical problem of reasoning about real algorithms. Rigorous reasoning is the only way to avoid subtle errors in concurrent algorithms, and we want to make reasoning as simple as possible by making the underlying formalism simple.
However, there is a debate between the PL approach (championed by Backus, Milner) and the specification approach (championed by Dijkstra, Lamport) over utility. The question is whether proving at the code level is empirically viable (at a reasonable cost) for all but the simplest of programs. Indeed, so far the answer seems to be no. There has been only one program ever written and verified using dependent types (CompCert), it is certainly non-trivial but rather small, yet it required a world-class expert, took a lot of effort, and even then required corner-cutting (Leroy says he gave up on proving termination, simply adding a counter and throwing a runtime exception if it runs out). TLA+, OTOH, is used extensively and regularly by Amazon (and Oracle, Microsoft and others), by "plain" engineers, on real-world large systems (far larger than CompCert), and management loves it because it actually seems to save them time and money. This is only possible because TLA+ is not the programming language.
Lamport doesn't reject the theoretical possibility of a PL that could provide large-scale verification of some sort (end-to-end verification will always be extremely expensive due to simple complexity arguments), only points out that no PL has so far come anywhere close to fulfilling this promise. Of course, TLA+ doesn't provide end-to-end verification, but that is too expensive -- and unnecessary -- for 99% of the industry anyway. I think that the ideas are compatible, but so far in theory only, while in practice they are not (yet?).
Has there ever been another non-trivial real-world program written in Coq (or another dependently-typed language for that matter) other than CompCert?
> Didn't know people actually used TLA.
Oh, far more than Coq; possibly more than Isabelle, even. TLA+ was designed for engineers, and evolved along with careful observation of how it is used by them. Coq is mainly used by type theoreticians to explore proving various mathematical theorems using ITT, and by PL people exploring various PL theories. TLA+ is used by engineers for large-scale software[1][2][3].
> I'd still want a it embedded in a hosting type-theory so I can use it both for proofs and macros.
I'm not sure what you mean by macros (I'm not a type-theory person in the least), but what does it matter if it's a type theory or a set theory? Lamport's thesis was that just as virtually all math proofs don't require type theory, neither do program proofs; indeed virtually none of the algorithm proofs in computer science employ type theory at all. TLA+ is a formalization of such proofs.
The main advantage of TLA+ is that it's as powerful as Coq for verifying algorithms (though it is not designed for proving general mathematical theorems), yet it any engineer can master it in weeks, without learning any new (not to speak of rather exotic) math. Also, it is amenable (and indeed supports) to model-checking, which alone is enough to make it practical. Deductive machine-checked proofs (which TLA+ also supports) are just too time consuming, and have ever been used on full programs only a handful of times. Their main use in industry is to tie together model-checked programs[4].
TLA+'s disadvantage is that it's very hard to extract a program from a TLA+ spec. Translations going the other way (from code to TLA+) have been done a number of times (for C and Java) but only in academia AFAIK. But this is unsurprising as Lamport's (and Dijkstra's) thesis is that effective, practical, program verification can only be done at a level higher than program code (unless it's a small program, specifically written in a simplified matter for the sake of verification, and the very large effort is acceptable -- all three conditions that have been met in the few cases where deductive, whole-program verification has ever been used).
EWD1303:
> The profound significance of Dekker's solution of 1959, however, was that it showed the role that mathematical proof could play in the process of program design. Now, more than 40 years later, this role is still hardly recognized in the world of discrete designs. If mathematics is allowed to play a role at all, it is in the form of a posteriori verification, i.e. by showing by usually mechanized mathematics that the design meets its specifications; the strong guidance that correctness concerns can provide to the design process is rarely exploited. On the whole it is still "Code first, debug later" instead of "Think first, code later", which is a pity, but Computing Science cannot complain: we are free to speak, we don't have a right to be heard. And in later years Computing Science has spoken: in connection with the calculational derivation of programs —and then of mathematical proofs in general— the names of R.W. Floyd, C.A.R. Hoare, D. Gries, C.C. Morgan, A.J.M. van Gasteren and W.H.J. Feijen are the first to come to my mind.
Backus as quoted in EWD692 (Djikstra attacks this):
> One advantage of this algebra over other proof techniques is that the programmer can use his programming language as the language for deriving proofs, rather than having to state proofs in a separate logical system that merely [sic!] talks about his programs.
From a perspective of a PL person like myself, these ideals are very compatible. Without correctness by construction, there is not enough proof reuse so formality will forever be doomed for niche applications (aka computers embedded in dangerous things). Likewise after trying out intuitionistic type theory--based things (e.g. Agda) separating the program and proof langauges just seems clumsy. Overall separating programming and proof whether spatially (seperate languages) or temporally (correctness proved after the fact) is bad, and the reasons hardly depend on the dimension of separation