Lambda the Ultimate

Modern Eiffel is a new language which is syntactically based on Eiffel but has a lot of concepts of functional languages like Haskell, OCaml or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a compiler can statically check that a programm written in Modern Eiffel meets its specification.

The following article describes how Modern Eiffel's proof engine can be used to reason with inductive types.

Here's a fun challenge for LtU. The team at Securelist is analyzing a worm called Duqu and found a few interesting things. One of them is that they can't figure out the source language for the core framework.

After having performed countless hours of analysis, we are 100% confident that the Duqu Framework was not programmed with Visual C++. It is possible that its authors used an in-house framework to generate intermediary C code, or they used another completely different programming language.

We would like to make an appeal to the programming community and ask anyone who recognizes the framework, toolkit or the programming language that can generate similar code constructions, to contact us or drop us a comment in this blogpost. We are confident that with your help we can solve this deep mystery in the Duqu story.

I'm not clear on how much knowing the source language helps with the security analysis, but what else were you doing with your time? All the details and clues in the object file can be found on their blog.

Few Examples of Lisp Code Typography, spanning 54 years, collected by Newlisp's Kazimir Majorinc.