Re: [arch-d] I-D Action: draft-iab-protocol-maintenance-08.txt

["[e-mail]" <[e-mail]>]

—
Dr. Joe Touch, temporal epistemologist
www.strayalpha.com

> On Jul 13, 2022, at 5:52 AM, Martin Thomson <[e-mail]> wrote:
> 
> On Wed, Jul 13, 2022, at 15:08, [e-mail] <mailto:[e-mail]> wrote:
>> Additionally, there’s the difference between the state machine and the 
>> implementation; the idea at one point was to generate both the state 
>> machine and the protocol implementation from the same description, but 
>> it never fully developed.
> 
> Like miTLS[1]? That's a functional implementation based on a verified state machine. It's not a practical implementation, but it comes pretty close. There's a gap, sure, but it isn't as big as you might think.
> 
> [1] https://mitls.org/ <https://mitls.org/> (same folks as last time)

Verified = does what the protocol says, which is not the same as testing for specification errors that could cause races or other corner cases.

Additionally, “not a practical implementation” is a show-stopper; there’s little point to an implementation that “proves you can derive code from a spec” when you operationally don’t end up using that code. The fact that the release is written in two languages - one for spec, one for implementation, neither of which is the one used for verification, basically underscores my observation.

Joe