*type safety*means (remember: progress + preservation) and we have studied this notion time and again for some of the TAPL languages. However, I don't feel like the notion really sinked in universally. Some students consider all this semantics and calculus stuff as obscure and there is a certain critical mass of notation, when passed, concepts are not understood anymore (by some if not many of the Bachelor-level students in my class).

Last night, I came up with a nice "semantics riddle" for type safety:

**What would be a super-trivial language with a type system and an SOS semantics such that type safety is violated?**

I gave the students 2 minutes to think about the question.

I emphasized several times that the language should be super-trivial.

I also asked them for a general strategy for mis-designing a language to be type-unsafe.

One idea that popped up was to support some notion of cast.

We agreed that this would not be trivial, certainly not super-trivial.

Here is my reference solution:

**Syntax of expressions**

*e* ::= *v* | *z*

(Hence, there are expressions (forms) *x*, *y* and *z*.)

**Values (normal forms)**

*v* := *x* | *y*

**Types**

*t* ::= *a* | *b*

(*a* and *b* are the possible types.)

**Small-step relation**

*z* -> *x*

(Yes, we only have one axiom.)

**Typing rules**

x : a

y : b

z : b

(Yes, we have only axioms here.)

**Demonstration of lack of type safety**

The term *z* is the culprit.

*z *: *b* but *z* -> *x* and *x* : *a*

Regards,

Ralf

More trivial solutions are possible with unityping and a lack of progress instead of a lack of preservation. A very degenerate case is

ReplyDeleteterm syntax

e ::= x

types

t ::= a

typing

x : a

values

none

reduction

none

So we have neither a reduction semantics for x nor is x a value.

But maybe that's too trivial to be a language? ;-) I'll try again

term syntax

e ::= x | y | z

types

t :: = a

typing

x : a

y : a

z : a

values

v ::= y

reduction

x -> z

So x reduces to z which has no defined reduction yet isn't a value.