Re: [Scheme-reports] Formal comment: The denotational semantics

[Aaron W. Hsu <arcfide@x>]

"Perry E. Metzger" <perry@x> wrote:

> On Fri, 6 Jul 2012 01:42:06 -0400 John Cowan <cowan@x>
> 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 | arcfide@x | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.

_______________________________________________
Scheme-reports mailing list
Scheme-reports@x
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports