Lambda the Ultimate

Hello,

I'm currently designing an intermediate programming language, with its virtual machine and compiler. The goal is to provide language designers a common runtime framework easy to target, well optimized, and a good set of librairies.

The language is designed to support a wide kind of semantics and type systems (static and dynamic) and offers all together imperative, OO, and functional features. It might be quite easy to generate from your favorite language to this intermediate language. This way, you can use either a safe small and embedable VM or a full speed JIT to run the code.

For reusing the libraries, you might have to write some wrappers for your language semantics but that's still less work than doing C/C++ FFI.

I'm planing to release soon the full specifications of the language with an OCaml toy interpreter, and will welcome any comments. VM and JIT will follow later.

But before that, what do you think about this project ? Will you feel like using this runtime system ? and what kind of features are you excepting to be in the specs ?

By itself, this paper is not related to PLT. However, it is interesting to observe how an idea of "types up to isomorphism" manifests itself in different communities - called data equivalence of (nested) relational schemes in this paper.

I wonder, how reformulation of the paper in CT terms would look like, and whether it will be data-equivalent to the original :-)

Restructuring Partitioned Normal Form Relations Without Information Loss

PS: I hope this is not too much off-topic.

During a discussion on the subject of passion in programming, David Bremner on #haskell pointed out Richard Hamming's 1986 talk You and Your Research. Here's a taste:

At Los Alamos I was brought in to run the computing machines which other people had got going, so those scientists and physicists could get back to business. I saw I was a stooge. I saw that although physically I was the same, they were different. And to put the thing bluntly, I was envious. I wanted to know why they were so different from me. I saw Feynman up close. I saw Fermi and Teller. I saw Oppenheimer. I saw Hans Bethe: he was my boss. I saw quite a few very capable people. I became very interested in the difference between those who do and those who might have done.

Hamming clearly describes both the difference between the two and how you can be one of those who do.