previous  next  contents  top

My Comments, Impressions, Summaries of conferences, talks, and papers

 


 

Principia Mathematica is modern and insightful

Principia Mathematica by Whitehead and Russel was published back in 1910 -- and yet it reads like a modern text on programming languages. I have found Principia quite engaging and hard to put away. Principia discusses, with great insight, such modern topics as extensionality/intentionality, referential transparency, type. It contains perhaps the first mentioning of `domain', `alpha renaming' and `type' in the modern sense. Its `incomplete symbols' -- the ones that only make sense in a context -- anticipate continuations and control operators. It insightfully observes that the notions of free and bound variables, substitution, abstraction, and application all come from linguistics. I could not help but feel that Principia already contained lambda-calculus. It also seems that Russel and Whitehead anticipated intuitionism, for example, when insisting on separate notations for 'any' vs. `all' (although admitting the equivalence of these notions in their theory).
Version
The current version is 1.2, June 2007.
References
< http://name.umdl.umich.edu/AAT3201.0001.001 >
Principia Mathematica by Alfred North Whitehead and Bertrand Russell. Cambridge: University Press, 1910-
The full scanned text, many thanks to The University of Michigan Historical Mathematics Collection

PrincipiaMathematica.txt [7K]
Notes taken while reading Chapter 1 of Principia, with several comments very kindly given by Jacques Carette.

 

Functional Approach to Texture Generation

This is the summary of the talk given by Jerzy Karczmarczuk at PADL02 in January 2002. The talk describes 'Clastic', a system for generation of procedural textures.

It is common to operate on matrices and pixelmaps by reading and writing the (i,j)-th element or pixel. There is, however, a dual approach: rather than manipulate pixels we manipulate functions that manipulate pixels. The result is surprisingly concise and lucid, let alone coordinate- and storage-independent.

The pure functional library of texture generators has been used in teaching, of functional programming and of computer graphics. The Clastic web site and the tutorial show many intricate and exquisite textures, described declaratively, combinatorially -- often by an order of magnitude shorter than in the traditional, imperative, pixel-shoving approach. Furthermore, the sequences of combinators can be subjected to automated deforestation based on fusion laws.

The coordinate-free way of describing textured objects reminds one of the coordinate-free formalism of Geometric Algebra and of the General Covariance principle of Relativity (or, the General Coordinate Invariance principle).

Version
The current version is 1.0, Jan 2002.
References
Clastic-summary.txt [5K]
The summary of Jerzy Karczmarczuk's talk along with some Haskell code paraphrased from the original Clean code.
It was posted, with a comment, as Re: Not quite enough abstraction on the SRFI-25 mailing list on Mon, 28 Jan 2002 21:10:10 -0800 (PST). That SRFI-25 thread includes Brad Lucier's message urging more abstraction in programming with vectors and matrices.

< http://users.info.unicaen.fr/~karczma/Work/Clastic_distr/clastic.html >
The Clastic Web site. It refers to the tutorial with many beautiful pictures.

 

Machine reasoning about machines: ACL2 theorem prover

This is the summary of the invited talk by J. Strother Moore at PADL2002 on January 20, 2002. The talk was about history, abilities and lessons of the ACL2 prover and its predecessor ``The Boyer-Moore Theorem Prover (NQTHM)''. Boyer and Moore were influenced by the insight that proving theorems by resolution was programming in predicate calculus. This insight was fully realized in ACL2, which is written in a pure-applicative (i.e., pure functional) subset of Common Lisp. The theorem specification and the implementation languages become the same! That means that the prover can prove a part of itself. Furthermore, since the ACL2 specification is the Common Lisp code, it can be compiled and executed. One can not only prove properties of a specification, but also run it directly, which gives us a provable implementation. That fact turned out quite useful when proving correctness of the AMD Athlon floating point unit.

J. Strother Moore remarked that his experience of writing and maintaining the imperative prover NQTHM for 18+ years, and the similar 11-year experience for the pure-functional ACL2 prover showed the applicative style is better. He said that he will never go back to the imperative style.

Version
The current version is 1.0, Jan 2002.
References
ACL2-summary.txt [10K]
The summary of the talk

< http://www.cs.utexas.edu/users/moore/best-ideas/nqthm/index.html >
The Boyer-Moore Theorem Prover (NQTHM)

< http://www.cs.utexas.edu/users/moore/best-ideas/acl2/index.html >
ACL2 summary and innovations

< http://www.cs.utexas.edu/users/moore/acl2 >
ACL2 home page

< http://www.cs.utexas.edu/users/moore/ >
J. Strother Moore home page

 

Protocol design, closures in OS systems programming, and other summaries from USENIX 2001

The following document is a collection of summaries and subjective impressions of USENIX 2001 Annual Technical Conference, June 28-30, 2001, Boston, MA. The talk by Radia Perlman on Myths, missteps, and folklore in protocol design was the best, the most informative let alone the most entertaining talk of the conference. For the first time I realized that the existing TCP/IP framework is not technically the best solution, and is fraught with problems (e.g., related to multicast). Far better approaches existed, such as CLNP. Unfortunately, they were rejected for purely political reasons.

Another notable talk was by David Mazieres on a toolkit for user-level file systems. The toolkit, SFS, lets us write asynchronous RPC servers, e.g., user-level NFS daemons. Asynchronous RPC programming largely follows the continuation-passing style. The toolkit therefore relies on numerous C++ template hacks to create a closure (of a partially evaluated function), to capture continuations, and to do reference-counting-based automatic memory management. During the discussion, a person asked why such a helpful and needed toolkit as SFS hasn't been implemented before. David Mazieres replied that he first tried to write SFS in plain C. The complexity of memory management for closures and continuations was staggering. He gave up. It's only now, David Mazieres said, that C++ provides features such as partial template instantiation that make it possible to write memory management and continuation-handling hacks. This reply certainly begs a question of using a better language, with garbage collection, closures and continuations built in.

The following talks are summarized:

Version
The current version is 1.0, Jul 6, 2001.
References
USENIX01-impressions.txt [36K]
The collection of summaries (in the outline format)

 

Limitations of threads, and other summaries from USENIX 2002

The document referenced below is a collection of summaries and subjective impressions of USENIX 2002 Annual Technical Conference, June 14-16, 2002, Monterey, CA. The topic of threads was discussed in several talks. The talks, perhaps unwittingly, confirmed that John Ousterhout was right after all: threads are really a bad idea, for most of the purposes. Several presentations have demonstrated why system developers and kernel hackers should know about continuations. Another notable point, expressed by a C programmer and a serious X windows developer, was that good ideas do come up just from mere writing down a formal specification. Software engineers and OpenSource developers should use Math and Logic.

The following talks are summarized:

Version
The current version is 1.0, Aug 23, 2002.
References
USENIX02-impressions.txt [58K]
The collection of summaries (in the outline format)

 

Neal Stephenson's keynote, a Logic File System, and other summaries from USENIX 2003

The following is a collection of summaries and subjective impressions of USENIX 2003 Annual Technical Conference, June 12-14, 2003, San Antonio, TX. Two presentations stood out. The first one was the keynote address by Neal Stephenson, the author of Cryptonomicon, Snow Crash, The Diamond Age, and the upcoming Quicksilver. He started his insightful presentation with an observation that programmers and professional writers have a lot in common. In particular, both groups build complex mental structures, which they must then serialize through a keyboard by pressing one key at a time. Neal Stephenson convincingly argued against a so-called distillation theory, which, in the realm of writing software, corresponds to a software development methodology, or the process. Good books are not written by systematically refining bad drafts. Likewise, it is futile to hope that good software can eventually be produced by inept programmers following a systematic process. Neal Stephenson also stressed the importance of giving ideas time to mature, in the subconsciousness, so only good ideas percolate to the conscious level.

The most innovative talk was ``A Logic File System'' by Yoann Padioleau and Olivier Ridoux. The talk attempted to bring filesystems from the age of hierarchical and network databases into the age of relational -- and, moreover, deductive databases -- and yet maintain the familiar cd, ls, mkdir, mv interface, file paths and shell globs. The central idea is an automatic grouping of query results into navigatible `subdirectories' according to the most general and meaningful attributes. Embedding a Prolog interpreter into a file system and viewing file paths as logical formulas are very insightful and inspiring. The file system is implemented, has been used in practice and shows good performance.

The following talks are summarized:

Version
The current version is 1.0, Jul 14, 2003.
References
USENIX03-impressions.txt [57K]
The collection of summaries (in the outline format)

 

Software development at Pixar, relevance of academia to industry, and other summaries from USENIX 2006

These are subjective notes on the USENIX 2006 Annual Technical Conference, June 1-3, 2006, Boston, MA. The notes summarize invited talks and panels -- in particular, the talk by Greg Brandeau, Vice President of Technology at Pixar Animation Studios, about the whole process of making animated movies, the supporting software and hardware, and the help Pixar needs from software developers. Also of note were panels about Open Source business models and the relevance of university (systems) teaching and research to industry.

Version
The current version is 1.0, June 17, 2006.
References
USENIX06-impressions.txt [27K]
The collection of summaries (in the outline format)

 

Distinction between Scheme and Lisp, from one day of the International Lisp Conference ILC2002

The following subjective impressions of one day of the International Lisp conference ILC2002 include an unenthusiastic opinion of the `Water' programming language, and the critique of the statistical approach to knowledge -- of the `Google Way'.

My overall impression from ILC02 was that Lisp and Scheme, despite the common syntax, are different languages and communities. I think Python is closer to Haskell than Lisp is to Scheme. Common Lisp (CL) seems to me like a Smalltalk with round parentheses. Scheme community is more diverse, valuing the functional approach. In contrast, CL community seems more pragmatic and more ad hoc. The CL code I saw was object-oriented, stateful, and Smalltalk-like.

Version
The current version is 1.0, Nov 12, 2002.
References
ILC02-impressions.txt [15K]
The collection of summaries (in the outline format)


Last updated December 7, 2007

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML