Paul Rubin wrote:
> "Diez B. Roggisch" <[EMAIL PROTECTED]> writes:
>
>>>Which implies that even in ADA, runtime type errors are in fact
>>>expected - else there would be no handler for such a case.
>>
>>Well, yes, runtime errors occur - in statically typed languages as
>>well. That's essentially the halting-problem.
>
>
> Well, no, it's quite possible for a language to reject every program
> that has any possibility of throwing a runtime type error. The
> halting problem implies that no algorithm can tell EXACTLY which
> programs throw errors and which do not. So the language cannot accept
> all programs that are free of runtime type errors and reject all
> programs that definitely have runtime type errors, with no uncertain
> cases. But it's fine for a language to reject uncertain cases and
> accept only those which it can rigorously demonstrate have no type
> errors.
Also, if you're really into this, read this DEC SRL report on
Extended Static Checking for Java, a system from the 1990s.
ftp://gatekeeper.research.compaq.com/pub/DEC/SRC/research-reports/SRC-159.pdf
They were doing great work until Compaq bought DEC and killed off research.
The follow up to that is Microsoft's Spec# effort, which is program
verification for C#. See
http://research.microsoft.com/specsharp/
They have some of the same people, and some of the same code, as the
DEC effort.
Back when I was working on this, we only had a 1 MIPS VAX, and theorem
proving was slow. That's much less of a problem now.
John Nagle
--
http://mail.python.org/mailman/listinfo/python-list
