[r6rs-discuss] Re: [Formal] Allow compilers to reject obvious violations

From: Matthias Felleisen <matthias>
Date: Sun Feb 25 14:26:58 2007

On Feb 25, 2007, at 12:00 PM, r6rs-discuss-request_at_lists.r6rs.org wrote:

> 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.

Correct. Drop the "or not".

> 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?

1. This is a truly strange remark from the editor of three reports
that attempted to specify the meaning with a denotational semantics.
My own research has suggested time and again that denotational
semantics isn't truly up to the task in many cases so I prefer
operational semantics, like SML's. The one that comes with R6RS has
the advantage that it is a semi-algorithm.

2. "Type systems" or perhaps "rejection systems" -- meaning systems
that prevent programmers from running an expression -- should have
the property that they are algorithms. I suspect you agree with that
much.

I think it would therefore be the "right thing" to specify them as
such explicitly not implicitly via the report. There is nothing
whimsical about asking for an algorithm to be spelled out in an
algorithmic language.


>> 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 ...

No, see above. -- Matthias

P.S.

> 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.


I don't consider the four soft type systems for Scheme that I have
been involved with "type systems" or "rejection systems". None of
them prevented anyone from running a program.
Received on Sun Feb 25 2007 - 14:26:48 UTC