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

[Chad Perrin <perrin@apotheon.com>]

On Fri, Dec 22, 2006 at 12:03:09PM -0800, David Brown wrote:
> 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.

This all seems rather simple to me:

It's type-safe if you cannot get type errors without subverting the type
system.

-- 
CCD CopyWrite Chad Perrin [ http://ccd.apotheon.org ]
This sig for rent:  a Signify v1.14 production from http://www.debian.org/