Re: Compile Time vs. Run Time, Mixed Language Compiling, Fat Code

J.Giles wrote:
JG [...] The article I was responding to made claim that
JG programs which pass the typechecker of a strictly typed language never
JG have bugs (the exact statement was " An SML program which successfully
JG typechecks will not bomb at runtime").


"Never to have bugs" and "not to bomb at run-time" are two different
things, and the difference is important in this particular discussion
about what a type-system can do for you.
A program might have bugs without ever bombing:
- it could simply produce the wrong results (for some inputs)
- it may not terminate, although it is supposed to
- it may terminate, although it is supposed not to (operating
    systems, for example)


Errors of this form are not captured by SML type checking.


Some errors, like opening non-existing files, division by zero, etc. live
within SML (and its type system) as so called "exceptions". You can catch
them and continue with some other computation, but if an unforeseen
exception is raised (SML terminology), then your program terminates with a
corresponding error message.


JG This latter is clearly wrong. Not only *CAN* programs which are free of
JG type errors still contain bugs, those remaining bugs are the hardest to
JG find and correct: they account for the vast majority of debugging time.


I am not so sure about that. I remember having made errors in C programs,
which took me quite a while to debug but which would have been caught by a
stricter type-system. A type-system also finds some errors which hardly
ever show up, because the buggy code bit is hardly ever executed. These
errors are often easy to find _when_you_look_for_them_, but you don't,
until 6 months after distributing the program you get a bug report from a
frustrated user [yes, this is autobiographic] . Thus, some hard-to-find
errors are detected by type-checking. On the other hand, if a program
behaves wrongly by giving the wrong result, then debugging is already
slightly simplified as the wrong result (e.g. the unforeseen exception)
gives you a first clue what is going wrong. The cause of an illegal
termination/non-termination may be difficult to find though.


JG In fact, I would be surprised if SML were so restrictive as to guarantee
JG bomb-free code once you pass the typechecker. [...]


It does, although one has to be precise what "bomb" actually means (and
the compiler has to implement the fancy bits correctly -- the New Jersey
SML compiler for example has some limitations). For getting a more
precise picture about this, I recommend Xavier Leroy's PhD thesis
"Polymorphic Typing of an Algorithmic Language", which contains some
suggestions for the strengthening of the SML type-system including
soundness proofs. "Soundness" in this context is exactly the absence of
bombs on run-time for any well-typed program. [The thesis (or rather its
translation into English) is ftp'able from nuri.inria.fr, file
INRIA/publication/RR-1778.ps.Z.]


Stefan Kahrs
--

Return to the comp.compilers page.
Search the comp.compilers archives again.