On Mon, Mar 8, 2010 at 9:32 AM, Michael Arnoldus <[email protected]> wrote:
> Ok - that makes sense. Good point. > > Would it be fair to say that we're really searching for is a formally > specified processor that makes the programmer as efficient as possible? > > Michael > > We're searching for a way to solve orthogonal problems orthogonally. Specification is completely separate from implementation. The AUSTIN Protocol Compiler project [1] has a really good example of TCP/IP Networking stack as implemented in BSD 4.4 and presented in Wright and Stevens TCP/IP Illustrated Volume 2. They argue that, if you look at the C language implementation: [...] important details handling intrinsic or extrinsic issues frequently comprise only a small fraction of the implementation, while these details require a great deal of research and constitute the largest part of the difficulties in protocol development. For example, Nagle's algorithm[9], which adaptively inhibits small messages in TCP connections and thus helps to avoid network congestion collapse, requires approximately four lines of code in TCP/IP Illustrated's presentation. Refinements to Nagle's algorithm, originally published in 1984, are still being suggested; for example, by Minshall, et al., in 1999 [10]. The key to understanding and implementing any complex system with vital but miniscule details, particularly in such an ad-hoc environment, is modularization. In case of network protocols, modularization almost always involves layering. Hopefully, if you're on this mailing list, you're familiar with Ian Piumarta's work on A Minimal Architecture for TCP/IP [2]. Unfortunately, Ian has not written a full technical report on this subject. If he did, it would make sense to cite the Austin Protocol Compiler project, as it appears to be the most advanced project in terms of addressing orthogonal (TCP/IP) networking problems orthogonally. In other words, using approaches to building operating systems other than just the layering approach describes by Dijkstra in The Structure of the 'THE'-multiprogramming System [3] and also the aspect-oriented approach by Kiczales [4], which is commonly confused by researchers and practitioners as being what Dijkstra meant by "the separation of concerns" [5], what Christopher Strachey meant by "*Figure out* what you want to *say* before you *figure out* how to *say* it" [6], and what Joseph Goguen ambitioned for OBJ and TATAMI, using such powerful ideas as inductionless induction as an example of "proof-by-consistency" [7]. Informal list of references [1] http://books.google.com/books?id=P4vmo2Sdjg8C [2] A Tiny TCP/IP Using Non-deterministic Parsing, http://vpri.org/pdf/tr2007008_steps.pdf - Page 17 [3] http://userweb.cs.utexas.edu/users/EWD/transcriptions/EWD01xx/EWD196.html [4] The Art of the Metaobject Protocol, by Gregor Kiczales, Jim des Rivieres and Daniel G. Bobrow. 1991. [5] http://userweb.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD447.html [6] Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, by Joseph Stoy. 1977. See preface for quote. [7] "Tossing Algebraic Flowers Down the Great Divide." Joseph Goguen.
_______________________________________________ fonc mailing list [email protected] http://vpri.org/mailman/listinfo/fonc
