Re: Why Amazon Chose TLA+

[ernie...@xxxxxxxxx]

On Tuesday, March 31, 2015 at 8:27:02 PM UTC-4, Leslie Lamport wrote:
Hi Leslie,

> As expected, we are having an agreement.  
I agree.

>    Many interesting protocol specifications don't require existential
>    quantifiers...
> I'd probably characterize those "interesting protocol specifications"
> as high-level designs from which people code.  

Sorry for the ambiguity, I meant the parsing to be (interesting protocol) specifications, not interesting (protocol specifications). That is, there are interesting protocols (e.g. Paxos) whose specifications (at most one value chosen, and ... implies some value chosen) require at most trivial quantification. Someone who understands nothing about why Paxos works can therefore check Paxos (or any other protocol for consensus) with TLC.