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

Hi everyone,

I just wanted to share that we had a very productive meeting of the EDM
programme this morning where draft-iab-protocol-maintenance was discussed.
The editors got incredibly constructive feedback that we plan on
incorporating in the near future. Give us a few weeks to do that and submit
a new revision and then we'll notify this list.

Thanks,
David

On Mon, Jul 18, 2022 at 8:46 AM Rob Wilton (rwilton) <rwilton=
40cisco.com@dmarc.ietf.org> wrote:

>
>
>
>
> *From:* Architecture-discuss <architecture-discuss-bounces@ietf.org> *On
> Behalf Of *touch@strayalpha.com
> *Sent:* 13 July 2022 16:18
> *To:* Martin Thomson <mt@lowentropy.net>
> *Cc:* architecture-discuss@ietf.org
> *Subject:* Re: [arch-d] I-D Action: draft-iab-protocol-maintenance-08.txt
>
>
>
>
>
> —
>
> Dr. Joe Touch, temporal epistemologist
>
> www.strayalpha.com
>
>
>
> On Jul 13, 2022, at 5:52 AM, Martin Thomson <mt@lowentropy.net> wrote:
>
>
>
> On Wed, Jul 13, 2022, at 15:08, touch@strayalpha.com 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/ (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.
>
>
>
> Going a bit off topic, but a colleague of mine gave an interesting talk on
> TLA+ (TLA+ - Wikipedia <https://en.wikipedia.org/wiki/TLA%2B>), which can
> be used to write formal specifications, and IIRC, it was definitely able to
> spot race conditions and bugs in the specifications (e.g., if the system
> transitioned to a state that was not valid).
>
>
>
> Of course, it doesn’t speak to whether a particular implementation
> conforms to a valid specification or not.
>
>
>
> Rob
>
>
>
>
>
> 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
> _______________________________________________
> Architecture-discuss mailing list
> Architecture-discuss@ietf.org
> https://www.ietf.org/mailman/listinfo/architecture-discuss
>