Proto for Boost mailing list page: Re: [proto] talking proto

Subject: Re: [proto] talking proto
From: joel falcou (joel.falcou_at_[hidden])
Date: 2010-07-18 02:30:23

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]