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

From: <bear>
Date: Sun Mar 11 13:52:07 2007

On Sun, 25 Feb 2007, Marcin 'Qrczak' Kowalczyk wrote:

>I believe there should be defined a set of potential programs, called
>e.g. statically valid programs, such that:
>
>- It includes all programs which are intuitively correct.
>
>- It's easy to determine whether a program is statically valid,
> without running it.

I think the largest class of "statically valid" programs that
can be found is going to be the subset of programs which are:

   a) already macroexpanded or contain no macro definitions
   b) do not contain any use of call/cc
   c) do not contain any use of eval
   d) possible to prove type-correct by the Hindley/Miller method
   e) there may be other restrictions I didn't think of.

This is a useful class, but there are an infinite number of correct
programs that are not within it.

>- A conforming Scheme implementation must accept all statically valid
> programs, and it must reject all programs which are not statically
> valid (modulo implementation extensions, resource constraints etc.).

No. Absolutely not. There is no way you can reject programs which
are not statically valid and still have a language which is useful
in the ways Scheme is useful. As I said, there are many correct and
useful programs which are not statically valid. There will always
be things which are true even though no reasonable compiler can prove
them. Sometimes those things are the invariants that allow the
programmer to prove that code is correct.

                                Bear
Received on Sun Mar 11 2007 - 13:51:27 UTC