> There is formal specification in the large if you count formal mathematics.
Sure, but TLA+ is not aimed at research. The biggest problem, by far, plaguing not just proof assistants but formal logic in general, pretty much since its inception, is complexity. Which is ironic because the entire purpose of formal logic -- from Leibniz's original dream to Frege's early success -- is to be simple, clear and easy tool for practitioners. Compared to the dismal failure of formal logic in achieving that (which was acknowledged and lamented by the likes of von Neumann and Turing, but has since been shrugged off even though the problem has gotten considerably worse), I think the fact that people who are not trained logicians use TLA+ to do real work makes it a crowning achievement not only in software verification but in the history of formal logic. To achieve that, TLA+ had to shed away everything that isn't absolutely necessary. Lamport once said after hearing a lecture about some proposed addition to TLA+: "it's taken you 6 months to add something to TLA+ that it had taken me 15 years to remove".
> It makes essentially no business sense to try to formally verify things past several thousand lines.
Well, we don't know how to do that in a way that would be feasible; I consider that a "limit" because the software we use and need is very commonly three orders of magnitude ahead of what deductive verification can handle. And the gap has been constant or even growing for the past 40 years or so.
> Again formal mathematics repositories are a counterexample.
I disagree. Formal mathematics is about taking years to prove a proposition that could be written in one or a couple of lines. I think that the resemblance between deductive mathematical proofs and deductive software verification is like that between painting the Sistine Chapel and painting a large hospital. The similarity is superficial.
> If you have one in the wild, I'd love to take a look to learn from.
> But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space ... but rather the difficulty in even expressing that idea.
Can you DM me on Twitter (get there from the about page of my blog: https://pron.github.io) or send me an email (my name at Google's mail service)? I'm curious to see the problem you're referring to.
> Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems?
Well, I don't yet understand the exact issue you're having, but no, I don't think that would be particularly helpful at all, for the following reason: If people wanted to modify Paxos itself, they can get their hands on Lamport's spec and tinker with it. If they want to use it as a component, then they can write an abstraction of it in a few line. All of TLA+ is about the abstraction/refinement relation (that is, IMO, what makes its theory cooler than Coq et al. for software).
> But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS.
Yep.
> One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.
Right, but we know more than to say it's just richness. We know exactly what kind of properties scale (through abstract interpretation, of which both type systems and static analysis are examples): inductive (= compositional) ones. I.e. a property such that if it holds for any state (whether or not reachable by the program), then any step in the program preserves it, or, alternatively, a property P, such that P(x) and P(y), where x and y are terms, implies that P(x ∘ y). Problem is that most functional correctness properties are not inductive/compositional for the language (i.e. that the above two description hold for any term in the language).
> That would be the closest to an alternative to formal specifications I could suggest.
I think that's one additional tool. But a knob that's easier to turn is soundness. The difference between verifying a property to 100% certainty and to 99.999% certainty can be 10x in cost, and as -- unlike mathematics -- an engineer is not interested in the correctness of an abstract algorithm but in that of a physical system that can always fail with some nonzero probability -- absolute confidence is never strictly a requirement. Of course, this is not just my opinion but it also seems to be that of many formal methods researchers, which is why concolic testing is such a hot topic right now.
I think that specification and verification must be separate -- i.e. you specify at any "depth" and then choose a verification strategy based on cost/benefit (so, no to dependent types), and in most cases, it's possible that concolic testing would be enough.
1. The very large Coq/Agda texts are usually large because of the proofs, not the specification/propositions. There's a 5-10x ratio, if not more.
2. I don't think that TLA+'s theory is intrinsically more "straightforward" than Agda's, even though it's certainly more familiar (I know some people who would insist that type theory is more straightforward than set theory). I think that a lot of work has gone into making TLA+ relatively easy to grasp; I think it's more design than a specific choice of theory, although the choice of theory certainly affects the design. In addition, as I've already mentioned, I think that TLA itself (i.e. not the set theory in the "+") is a particularly beautiful theory for talking about computation and discrete systems, that has some obvious advantages over the lambda calculus; in particular the abstraction/refinement relation that's the core of TLA (the semantic domain of TLA is a Boolean lattice where the less-than relation is behavior refinement).
Sure, but TLA+ is not aimed at research. The biggest problem, by far, plaguing not just proof assistants but formal logic in general, pretty much since its inception, is complexity. Which is ironic because the entire purpose of formal logic -- from Leibniz's original dream to Frege's early success -- is to be simple, clear and easy tool for practitioners. Compared to the dismal failure of formal logic in achieving that (which was acknowledged and lamented by the likes of von Neumann and Turing, but has since been shrugged off even though the problem has gotten considerably worse), I think the fact that people who are not trained logicians use TLA+ to do real work makes it a crowning achievement not only in software verification but in the history of formal logic. To achieve that, TLA+ had to shed away everything that isn't absolutely necessary. Lamport once said after hearing a lecture about some proposed addition to TLA+: "it's taken you 6 months to add something to TLA+ that it had taken me 15 years to remove".
> It makes essentially no business sense to try to formally verify things past several thousand lines.
Well, we don't know how to do that in a way that would be feasible; I consider that a "limit" because the software we use and need is very commonly three orders of magnitude ahead of what deductive verification can handle. And the gap has been constant or even growing for the past 40 years or so.
> Again formal mathematics repositories are a counterexample.
I disagree. Formal mathematics is about taking years to prove a proposition that could be written in one or a couple of lines. I think that the resemblance between deductive mathematical proofs and deductive software verification is like that between painting the Sistine Chapel and painting a large hospital. The similarity is superficial.
> If you have one in the wild, I'd love to take a look to learn from.
I wouldn't call it "in the wild", and it is used to bootstrap something fundamental (induction), but here: https://github.com/tlaplus/v2-tlapm/blob/master/library/Natu...
Also, search for "IsaM" here: https://github.com/tlaplus/v2-tlapm/blob/master/library/Well...
> But I do think it has problems with modularity. My state example wasn't to do with the difficulty of verification or the explosion of the state space ... but rather the difficulty in even expressing that idea.
Can you DM me on Twitter (get there from the about page of my blog: https://pron.github.io) or send me an email (my name at Google's mail service)? I'm curious to see the problem you're referring to.
> Wouldn't it be cool if people could import Lamport's Paxos spec directly into their own specs of their own systems?
Well, I don't yet understand the exact issue you're having, but no, I don't think that would be particularly helpful at all, for the following reason: If people wanted to modify Paxos itself, they can get their hands on Lamport's spec and tinker with it. If they want to use it as a component, then they can write an abstraction of it in a few line. All of TLA+ is about the abstraction/refinement relation (that is, IMO, what makes its theory cooler than Coq et al. for software).
> But an error message better than what amounts to red highlighting and "no" would be nice in TLAPS.
Yep.
> One knob you're leaving out though is the richness of the properties you're trying to prove. As you decrease the richness of the properties you can prove you can drastically decrease your burden. This starts bleeding into static analyzers and then if you dial the knob even further down into mainstream type systems. But the knob can be fairly low and still be useful.
Right, but we know more than to say it's just richness. We know exactly what kind of properties scale (through abstract interpretation, of which both type systems and static analysis are examples): inductive (= compositional) ones. I.e. a property such that if it holds for any state (whether or not reachable by the program), then any step in the program preserves it, or, alternatively, a property P, such that P(x) and P(y), where x and y are terms, implies that P(x ∘ y). Problem is that most functional correctness properties are not inductive/compositional for the language (i.e. that the above two description hold for any term in the language).
> That would be the closest to an alternative to formal specifications I could suggest.
I think that's one additional tool. But a knob that's easier to turn is soundness. The difference between verifying a property to 100% certainty and to 99.999% certainty can be 10x in cost, and as -- unlike mathematics -- an engineer is not interested in the correctness of an abstract algorithm but in that of a physical system that can always fail with some nonzero probability -- absolute confidence is never strictly a requirement. Of course, this is not just my opinion but it also seems to be that of many formal methods researchers, which is why concolic testing is such a hot topic right now.
I think that specification and verification must be separate -- i.e. you specify at any "depth" and then choose a verification strategy based on cost/benefit (so, no to dependent types), and in most cases, it's possible that concolic testing would be enough.