Eric Niebler wrote:
Joel, why write it in ML first?
Two reasons:

- ML is actually my first language so I can be quite productive with it. C++ is just my second one ;)

- ML has a strong type checker than help you not writing erroneous functions.
A classical thing is the match construct.

this is a function computing the size of a list.

let rec len x = match  x with
 |  [] -> 0
 |  x::xs -> 1 + len xs;

it's basically a listing of alternatives depending on how you parse the input thansk to the match ... with directive. If you "forgot" a case that make the function not working, ML will complain and in some case give you the missing case. Which means when your function is typed by ML, it has no more obvious error and should work ;)

Now, look at this again and replace let with template<class T> struct len and match by template specialization. Bingo, you got the exact same function turned into a meta-function.

So writing ML first help us test the meta-function (usually the large, complex meta-function we use in the semantic) with a proper level of error detection. Afterward, the transformation is rather simple and we know by transitivity of corretcness that the template is now working for every case. I've planned to get students working on such ML2C++ converter of meta-functions but never found a proper student able to take on this task

[Aside discussion]
That's a temporary solution though. What we may need is to have a formal description of C++ template in HOARE logic and proven with Coq or ISABELLE so we know when we write a template metafunction that is does what it does in all situation. But that's one of a longer time frame research project. And on the quesiton why do we want this ? Well, if we prove that the C++ code generator is "correct" under some assumptions, that this C++ generator is based upon a simpler language we can verify and that we take for granted the C++ compiler is OK, then we have a complete DSL -> C++ -> executable chain which is certifiable and formally proven. In some use cases (aeronautics and such) this provability is a requirements.
[/Aside discussion]

proto mailing list

Reply via email to