Chris Smith wrote: > Joachim Durchholz <[EMAIL PROTECTED]> wrote: > > Assume a language that > > a) defines that a program is "type-correct" iff HM inference establishes > > that there are no type errors > > b) compiles a type-incorrect program anyway, with an establishes > > rigorous semantics for such programs (e.g. by throwing exceptions as > > appropriate). > > So the compiler now attempts to prove theorems about the program, but > once it has done so it uses the results merely to optimize its runtime > behavior and then throws the results away. I'd call that not a > statically typed language, then.
You're assuming that type-correctness is an all-or-nothing property (well, technically it *is*, but bear with me). What if the compiler is unable to prove a theorem about the entire program, but *can* prove a theorem about a subset of the program. The theorems would naturally be conditional, e.g. `Provided the input is an integer, the program is type-safe', or time-bounded, e.g. `Until the program attempts to invoke function FOO, the program is type-safe.' Of course, we could encode that by restricting the type of the input and everything would be copacetic, but suppose there is a requirement that floating point numbers are valid input. For some reason, our program is not type-safe for floats, but as a developer who is working on the integer math routines, I have no intention of running that code. The compiler cannot prove that I won't perversely enter a float, but it can prove that if I enter an integer everything is type-safe. I can therefore run, debug, and use a subset of the program. That's the important point: I want to run broken code. I want to run as much of the working fragments as I can, and I want a `safety net' to prevent me from performing undefined operations, but I want the safety net to catch me at the *last* possible moment. I'm not playing it safe and staying where the compiler can prove I'll be ok. I'm living dangerously and wandering near the edge where the compiler can't quite prove that I'll fail. Once I've done the major amount of exploratory programming, I may very well want to tighten things up. I'd like to have the compiler prove that some mature library is type-safe and that all callers to the library use it in a type-correct manner. I'd like the compiler to say `Hey, did you know that if the user enters a floating point number instead of his name that your program will crash and burn?', but I don't want that sort of information until I'm pretty sure about what I want the program to do in the normal case. -- http://mail.python.org/mailman/listinfo/python-list
