Eric Niebler wrote:

Joel, why write it in ML first?

Two reasons:

## Advertising

`- 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 proto@lists.boost.org http://lists.boost.org/mailman/listinfo.cgi/proto