Re: strong/weak typing terminology (was Re: [Caml-list] Scripting in ocaml)

[David Brown <caml-list2@davidb.org>]

skaller wrote:

> This is not my understanding of what safe means.

> Your program is safe? Ok, so would you use it to
> control a nuclear reactor? Do you really think anyone
> cares if the reactor blows, whether the program
> core dumped, failed to core dump, or threw an exception?
>
> to me safe means 'cannot fail'. But perhaps i misunderstand:
> it would be interesting to see another definition.

This is certainly a good definition of "safety", but not one commonly
used when referring to type systems.  It also has problems with
undecidability, and trying to enforce it generally results in
programming languages or language subsets that are so restrictive that
general purpose programming becomes very tedius, or just impossible.
Even systems that put a lot of effort into this kind of safety (such
as SPARKAda) don't claim that they "cannot fail", but instead refer to
it as high-integrity.

Most references use phrases like "type safety", although this seems to
get different definitions depending on the user.  Although specific
instances in a program, the compiler might be able to statically
determine if an array bounds is going to be violated, this can't be
done in the general case.

So, I'm not sure how defining "safe" so high that it can't be
implemented is useful to anyone.  Those interested in this topic
should definitely read up on the Ariane 5 rocket's first launch.  For
efficiency considerations the developers disabled some of the runtime
constraint checks on data conversions, which resulted in this failure.

Dave