[e2e] Reacting to corruption based loss

Jon Crowcroft Jon.Crowcroft at cl.cam.ac.uk
Thu Jun 9 00:10:41 PDT 2005

actually, we have 2 pieces of work that makke this entirely reasonable

1. my colleagues have a paper at SIGCOMM coming up about using higher order logic
to prove TCP correct (including different implementations _and_ the socket layer

2. one of our PhD students has written an SSHd and other non trivial protocols in 
ocaml, and thus can avail himself of various model checkers and automatic proof systems
and (as it happens) his code has acceptable performance

the decrying of good computer science methodlogy because it might be too slow or not able to cope with
"real world" scale systems is simply OUT OF DATE.

In missive <42A721C3.D59F601D at attglobal.net>, Cannara typed:

 >>It seems supercilliousness is the real solution, eh Reed?
 >>"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!
 >>> A bonus question:  if you have two cesium clocks on the ends of a link,
 >>> they will tick simultaneously, so you should be able to send data
 >>> without any risk of skew, right?   And if you reduce the messages to
 >>> single photons, you should NEVER have any errors, because photons are
 >>> irreducible.   So if we pursue reductionism to its limit, there should
 >>> be no errors in our system at all.   It's all "Internet Hooey" - the
 >>> idea that congestion can't be prevented and corruption can't be detected
 >>> are just foolish notions that SONET would never have to deal with.
 >>> Cannara is right, the Internet is a completely idiotic idea, and the
 >>> North American Numbering Plan was all we ever needed.
 >>> :-)



More information about the end2end-interest mailing list