[e2e] Reacting to corruption based loss

Cannara cannara at attglobal.net
Fri Jun 10 12:33:09 PDT 2005

Every program is a theorem, and TCP implementations are perfect, so that's not


RJ Atkinson wrote:
> On Jun 7, 2005, at 22:38, David P. Reed wrote:
> > I really think we missed the boat by not just proving all network
> > components correct.   Errors are really unacceptable, given modern
> > mathematical proof techniques.
> >
> > Since Cannara believes that all erroneous packets can be reliably
> > detected and signaled on the control plane, we are nearly there.
> > Just put a theorem prover in each router, prove that the packet
> > will be delivered, and you don't even have to put it on the output
> > queue!
>      Given the amount of router CPU that would be needed to deploy
> S-BGP, and the amount of energy being spent in some quarters pushing
> deployment of S-BGP onto the operators, adding a theorem prover on the
> router CPU would be easy.  Good idea.
> :-)
> Ran

More information about the end2end-interest mailing list