<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 22, 2016 at 5:45 AM, Josh Adams <span dir="ltr"><<a href="mailto:josh.rubyist@gmail.com" target="_blank">josh.rubyist@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Should RFCs / protocols of this nature just come with something like a quickcheck model for their spec?</blockquote></div><br>In principle, protocols should come with two things:</div><div class="gmail_extra"><br></div><div class="gmail_extra">* A set of parser combinators which fit into a framework such as Meredith Patterson's Hammer. This would make it next to impossible to accidentally parse the protocol wrong and establish syntactically valid input. In an Erlang world, it would produce proper Erlang terms.</div><div class="gmail_extra"><br></div><div class="gmail_extra">* A QuickCheck specification. This would allow implementors to verify their protocol against a quasi-formal model which would greatly improve quality of software. Every implementation would be at least as precise as the QC model. A more ambitious solution would include a model closer to e.g. TLA+. Then one writes a compiler from TLA+ to a QC system and you can check real-world programs.</div><div class="gmail_extra"><br></div><div class="gmail_extra">I think the reason it is not done has to do with effort. Doing the right thing(tm) often takes an order of magnitude more time compared to the quick and dirty hack. Since software is built primarily on the basis of speed (time), people don't do the necessary work up front. Rather, it is baked on later, when the damage has been done. Up front modeling often changes the spec in ways which removes ambiguity and room for error.</div><div class="gmail_extra"><br></div><div class="gmail_extra">If we should start, *the* place to start is TLS 1.3 :P</div><div class="gmail_extra"><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature">J.</div>
</div></div>