"Perry E. Metzger" <[email protected]> wrote: > On Fri, 6 Jul 2012 01:42:06 -0400 John Cowan <[email protected]> > wrote: > > Perry E. Metzger scripsit: > > > > > A +1 for switching to an operational semantics. It would be > > > especially cool to develop an executable semantics... > > > > If we are to take the semantics seriously, I think it means > > developing one whose soundness can be established with a proof > > assistant. > > Agreed. (I had somewhat assumed it, in fact.)
As Eli has correctly pointed out, and some others have already referenced, there have been significant improvements in the formal semantics world and in Schemeland particularly that we should take into account. I think the existing R6RS semantics was done in a way that was compatible with the Redex system. This is a step forward from what we have now, and while it is not where I would want to see the semantics of Scheme end, if we are not going to invest real time into the semantics, then we should at least be considering using a system that has some level of mechanization in it, and with Redex we already have most of this work done for us. That is separate and different than what I hope we will do, which is to dedicate real effort and real time towards moving forward beyond what we already have in the Redex R6RS semantics. -- Aaron W. Hsu | [email protected] | http://www.sacrideo.us Programming is just another word for the lost art of thinking. _______________________________________________ Scheme-reports mailing list [email protected] http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports
