PrincipiaMathematica.txt [7K]
Notes taken while reading Chapter 1 of Principia, with several comments very kindly given by Jacques Carette.
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).
< http://users.info.unicaen.fr/~karczma/Work/Clastic_distr/clastic.html >
The Clastic Web site. It refers to the tutorial with many beautiful pictures.
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.
< 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
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:
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:
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:
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.
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.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML