|
> 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?). [1]: http://research.microsoft.com/pubs/64074/lamport-actions.pdf |
Even if I was programming in a separate language, I'd still want a it embedded in a hosting type-theory so I can use it both for proofs and macros.