
Proto : 
Subject: Re: [proto] talking proto
From: Eric Niebler (eric_at_[hidden])
Date: 20100718 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 listlike 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 metafunction.
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 metafunction (usually the large,
> complex metafunction 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 metafunctions 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
Proto list run by eric at boostpro.com