On Sat, Sep 6, 2014 at 2:21 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Fri, Sep 5, 2014 at 6:31 PM, Ben Kloosterman <[email protected]> wrote: >> "ad hoc parse rules and/or parse ambiguities." are common in nearly all >> languages - with good reason they have taken short cuts to get something out >> the door. > > For many languages that is so. None of those languages are languages that > anyone has attempted to do regular formal reasoning about successfully.
I agree with your points, but have you considered making the AST the normative format for BitC programs, for the sake of formal reasoning? Not that it's impossible or even impractical to formalize surface syntax, but for reasoning about surface syntax, the first step would probably be to apply a verified parser anyway. If the AST is normative, you get to skip that, and your spec is reusable with different surface syntaxes. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
