Whither Wombat?

We interrupt the sequence of posts on aspects of Wombat for a couple of planning posts. This one on language design “decisions”.

1. Under the influence of Bob Harper, and also guys from the Mercury team, I am giving up my flirtation with lazy evaluation. It has always been my expectation that Wombat’s good support for closures would cover this. I now realise that I also need to handle memoization well. Anyway a fair bit of thought needs to go into making memoized streams as convenient as lazy lists, and also covering other lazy data structures.
2. Also from reading Harper, I see that he has had the same issue as me with the overloaded use of the word “variable”. My solutions was to use “mutable”. However he has already invented the word “assignable”, and since we don’t need 2 words for the same thing, I will, at some point, change the doc from “Mutable” to “Assignable”.

More substantively is the issue of the status of laws/axioms. It used to be that these were just comments. Then languages started including them in an executable form, with a bit of handwaving “quickcheck style checking programs might use this”. That’s where Wombat came in, and the way it is specified in the doc.

But I don’t think this phase will last long. It is time to do it properly and prove all claimed properties:

• Primitive types will come with axioms describing their behaviour, from the X86/JVM/whatever manual.
• The semantics of other Types will be proved from the code implementing the semantics using the assumed (if primitive) or proved (if not) semantics of the implementation.
• Other things that need to be proved include:
• proving that a supplied specialization does indeed implement the same algorithm as the original;
• proving that the procedures linking one implementation to/from a more comprehensive one (usual the main one) are inverses (where the reverse is defined).
• …

Just as the time has come for programming to help mathematicians deal with complexity, so it is time for mathematics to help control the complexity of programming. While this looks really ambitious, the main plan is to get the syntax right so that it can be brought in later. It is expected that initially the only proofs will be “admitted” (as they say in Coq). However it is expected to be extremely useful to think clearly about what should be proved.

A key decision needs to be made about WCTL: Wombat Compile Time Language. While the plan is for it to be a Wombat DSL, in the short term, to get going, it seems like a good idea to start with some existing scripting language which is well integrated with some target machine. A possibility is Pure which has a good interface to LLVM, and also to C code which could call more obscure parts of LLVM (like Integer overflow).