Lambda the Ultimate

Some of you might have followed some of my posts during 2012/2013 where I described the design of a programming language which allows static verification.

The previous working title had been "Modern Eiffel" since my first attempt had been to create a variant of Eiffel which allows static verification. During the language design more and more weaknesses of Eiffel popped up which are in the way to do static verification. The most prominent weak point is that Classical Eiffel is not type safe.

The result of my language design activities is a new language which has some syntactic resemblance to Eiffel.

However semantically the new language now called Albatross is more like Coq or Isabelle because it has a functional core and it allows to state assertions and prove them.

The last to years I have worked on a compiler and verifier for the language. The effort clearly has been underestimated by me and the one-year project has already taken two years and the available implementation has still a lot of restrictions. However the theorem prover works quite well and it certainly will take some time to complete the compiler.

For those of you who know Coq you might enjoy the capabilities of the proof engine and enjoy the fact that there is no extra proof language and all proofs are expressed by pure statements in predicate logic. Proof automation is done by predicate calculus as well and no by an integrated language like Ltac. Therefore the language is easier to learn than Coq, because every programmer has a well developed intuition about logic.

You can find the downloadable version of the compiler and a language description at the Albatross website.

The paper:

Resourceable, Retargetable, Modular Instruction Selection Using a Machine-Independent, Type-Based Tiling of Low-Level Intermediate Code

Ramsey and Dias have a series of papers about making it ever easier to generate compiler backends, and the claim is that they produce decent code to boot. I wonder if this stuff has/will show up in compilers I can use? (Or, do you think it not actually matter, for some pragmatic reason or other?)

Abstract: We present a novel variation on the standard technique of selecting instructions by tiling an intermediate-code tree. Typical compilers use a different set of tiles for every target machine. By analyzing a formal model of machine-level computation, we have developed a set of tiles that is machine-independent while retaining the expressive power of machine code. Using this tileset, we reduce the number of tilers required from one per machine to one per architectural family (e.g., register architecture or stack architecture). Because the tiler is the part of the instruction selector that is most difficult to reason about, our technique makes it possible to retarget an instruction selector with significantly less effort than standard techniques. Retargeting effort is further reduced by applying an earlier result which generates the machine-dependent implementation of our tileset automatically from a declarative description of instructions' semantics. Our design has the additional benefit of enabling modular reasoning about three aspects of code generation that are not typically separated: the semantics of the compiler's intermediate representation, the semantics of the target instruction set, and the techniques needed to generate good target code.