[r6rs-discuss] [Formal] Allow compilers to reject obvious
William D Clinger
will at ccs.neu.edu
Sun Feb 25 11:14:30 EST 2007
I am posting this as an individual member of the Scheme
community. I am not speaking for the R6RS editors, and
this message should not be confused with the editors'
eventual formal response.
Matthias Felleisen wrote:
> > The current draft already mandates hundreds of runtime
> > exceptions whose whimsical purpose is to make programs
> > that violate the requirements of the R6RS less likely
> > to run to completion. Why should that kind of whimsy
> > be limited to run time?
> This is not true. The report comes with a formal and executable
> specification of the operational semantics of R6R Scheme. I can
> determine whether or not a program's behavior is within the
> parameters of this specification.
Just as soon as you solve the halting problem.
Why, by the way, do you regard the requirements of a
"formal and executable" specification as less whimsical
than the requirements of an informal specification?
> What I am asking for is an equally precise specification of the "type
> system." That's all. (And I would be happy with stylized English that
> spells out the analysis that compilers are expected to perform.)
Then you are already happy, because the current draft
already explains (*) which &violation exceptions an
implementation must raise, and my formal proposal
uses that notion to spell out the conditions under
which a compiler would be allowed to reject a program.
Before you come back and say it isn't a type system if
the compiler is "allowed" but not "required" to reject
a program, let me remind you that I can cite several
type systems with that property. A couple of them may
even have been devised by you and your students.
(*) The current draft's stylized English is often
unclear or ambiguous to the point of hilarity, just
like much of the stylized English that spells out the
analyses that compilers are expected to perform.
More information about the r6rs-discuss