PEP 3107 and stronger typing (note: probably a newbie question)

[John Nagle]

Paul Rubin wrote:
> "Diez B. Roggisch" <deets at nospam.web.de> 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