Does strong typing imply type safety?

241 Views Asked by At

I'm reviewing lecture notes for a compilers course, and one of the slides says:

Strongly typed languages guarantees that accepted programs are type-safe

However, I can't find any evidence of this elsewhere.

For instance wikipedia lists c++ as a language with strong typing, but also lists c as a language that isn't type safe.

So what's the deal? Are the slides wrong, or have I missed something?

Wikipedia's example of strong typing

1

There are 1 best solutions below

0
On BEST ANSWER

"Strongly typed" is not a very well-defined notion. It's probably best interpreted as synonymous to the more accurate memory-safe (i.e., a program can never corrupt its own memory through undefined behaviour).

In type theory, the terminology "strongly typed" is never used. Instead, one speaks of sound type systems. Moreover, any set of typing rules that isn't sound isn't typically regarded a proper type system at all.

In informal usage, "strongly typed" also is applied to "dynamically typed" languages, which, from a theoretical perspective, makes even less sense. In the terminology of type theory, these languages aren't even typed.

Long ago, Luca Cardelli has introduced a more coherent classification of language safety by distinguishing two independent dimensions: typed/untyped and safe/unsafe. Assembly is untyped and unsafe, C is typed but unsafe, JavaScript is untyped but safe, and Java or ML is typed and safe. See e.g. http://www.lucacardelli.name/Papers/TypeSystems.pdf