On Sat, Sep 6, 2014 at 1:29 PM, Matt Oliveri <[email protected]> wrote:
> On Sat, Sep 6, 2014 at 2:21 PM, Jonathan S. Shapiro <[email protected]> > wrote: > > 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? > Actually, I did. This was (more or less) the idea that let me adopt layout. I figured that we could adopt an XML or lisp-like serialization of the AST and reason from that. 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. Yes. The thing is, though: I need the tool regardless. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
