George Michaelson ggm at algebras.org
Mon Sep 29 06:41:12 UTC 2014

for two asynchronous, otherwise unconnected systems, using TCP/IP there is
a state transition sequence which can be shown to work if you stick to it.
There are also (I believe) corner cases when you send unexpected sequences,
and some of them have known behaviours

in that sense, the question: "does the RFC adequately document the state
transition sequences which are understood to be valid states and
transitions" is a well formed question.

Robin Milner, in his calculus of communicating systems tried to codify a
formal mathematics of async communicating systems. I don't know if anyone
either extended the idea(s) or applied it to TCP/IP.

Certainly I believe there are formally verified protocols. Thats a space
Erlang occupies isn't it?

On Mon, Sep 29, 2014 at 4:14 PM, Larry Sheldon <larrysheldon at cox.net> wrote:

> On 9/29/2014 00:32, Pete Carah wrote:
>> For that matter, has the*specification*  of tcp/ip been proven to be
>> "correct" in any complete way?
> I find that question in this forum really confusing.
> I thought all of the RFC-descriptions of protocols were taken to be
> statements that "if you do it this way, we think we can inter-operate" but
> at no time to be taken as "right" or "wrong".
> --
> The unique Characteristics of System Administrators:
> The fact that they are infallible; and,
> The fact that they learn from their mistakes.
> Quis custodiet ipsos custodes

More information about the NANOG mailing list