Re: Semantics Tools

Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen) writes:
>eifrig@beanworld.cs.jhu.edu (Jonathan Eifrig) writes:
>> Curiously, I was wondering something related: How many people are
>>using formal semantic methods to either (1) generate a compiler or (2)
>>prove a compiler correct in "real life?"


>At Oxford, we are studying the verification of compiling specifications,
>and their rapid prototyping using logic programming.


I think perhaps you're misinterpreting my posting, and I just want
to clarify my question: I'm curious as to whether or not any of the
semantics-based techniques for compiler generation have made it
"off-campus" into the real world. My rule of thumb is whether or not some
scheme has generated a compiler that is intrinsically interesting to
someone other than those who made it.


For example, the ORBIT compiler for Scheme was actually used at
Yale as its installed Scheme compiler, I believe, as part of its T system;
this is the earliest example of a continuation-passing style compiler that
I know of that made it out into the real world. (Earlier examples
welcomed!) Hundreds, if not thousands, of commercial products have been
made with lex/yacc parsers, moving LALR parsing into the real world.


But has anyone used, say, Lee's MESS system to make something like
the "Gorgunza C" compiler? And if not, why not?


ObRefs:


@string{scc86 = "Proceedings of the 1986 ACM SIGPLAN Symposium on Compiler
Construction"}


@inproceedings{kranz86,
author = "David Kranz and Richard Kelsey and Jonathan Rees and Paul Hudak
and James Philbin and Norman Adams",
title = "ORBIT: An Optimizing Compiler for Scheme",
booktitle = scc86,
year = 1986,
pages = "219--253"
}


@book{lee89,
author = "Peter Lee",
title = "Realistic Compiler Generation",
publisher = "MIT Press",
year = 1989,
series = "Foundations of Computing"
}
[Yes, ORBIT is the compiler in T. My impression from reading Lee's book
is that MESS is indeed pretty messy, not well enough packaged for others
to use. And packaging is important: yacc became the most widely used
parser generator not because it broke any new ground in LR parsing ("ya"
stands for "yet another", after all) but because it was a lot easier to
use than any of the others available in the early 1970s. -John]
--

Return to the comp.compilers page.
Search the comp.compilers archives again.