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

Subject: Re: [proto] talking proto
From: Eric Niebler (eric_at_[hidden])
Date: 2010-07-18 13:43:50

On 7/18/2010 2:30 AM, joel falcou wrote:
> 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.

I'm pretty sure I understand this. I briefly looked into OCaml, so this
is familiar. Are the alternates tried in order or is there some notion
of "best match" like with template specialzations?

> If you "forgot" a case that make the function not working, ML will
> complain and in some case give you the missing case.

How in the world is that computable in general? Is match...with
restricted to list-like thingies?

> Which means when your function is typed by ML, it has no more obvious
> error and should work ;)

Cool. So you're using this to validate your semantic actions?

> 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.

I object! The len function computes the length of a *runtime* list.
Obviously with template specializations we're no longer dealing with
runtime data structures. I don't see how to the two relate.

> 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

Good luck!

> [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]

In theory it should be possible to add a theorem prover to proto to
validate semantic actions, right? Not that C++ TMP is necessarily the
best tool for this.

-- 
Eric Niebler
BoostPro Computing
http://www.boostpro.com