[erlang-questions] Quickcheck'ing a protocol

[Jesper Louis Andersen]

On Thu, Sep 22, 2016 at 5:45 AM, Josh Adams <josh.rubyist@REDACTED> wrote:

> Should RFCs / protocols of this nature just come with something like a
> quickcheck model for their spec?


In principle, protocols should come with two things:

* 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.

* 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.

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.

If we should start, *the* place to start is TLS 1.3 :P



-- 
J.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20160922/70611c3d/attachment.htm>