Ein Weihnachtsgedicht

(C) Professor Fish, aka Ralf Lämmel

Stille Nacht! Unheilvolle Nacht!

Alles schläft; einsam wacht

nur der Bachelor-Student,

der nie pennt,

der nur rennt.

So viele Prüfungen, o weh!

So viele Prüfungen, o weh!

Stille Nacht! Unheilvolle Nacht!

Die wird wieder durchgemacht.

Bester Student, o wie lacht

bös' aus Deinem Gesicht

die Aversion gegen Bologna's Gericht.

So viele Regularien, o weh!

So viele Regularien, o weh!

Stille Nacht! Unheilvolle Nacht!

Was hat man nur aus dem Uni-Studium gemacht?

Es ist nicht Bologna allein.

Andere Trends reihen sich hier ein.

Das Denken an Deutschland in der Nacht,

hat auch den Professor um den Schlaf gebracht.

Lautes Land! Unheilvolles Land!

O Marx, gib mir Eltern,

die Kinder fordern anstatt Lehrer zu quälen.

O Lenin, gib mir Erstsemester,

die wissen wollen anstatt videozugamen.

Früher war alles besser, o weh!

Früher war alles besser, o weh!

Stille Nacht! Unheilvolle Nacht!

Soll es Weihnachten nun sein,

dann Tod den Enten und glühe der Wein.

Der Wunschzettel ist auch schon da.

Merkel & Co. machen es klar.

Merkel & Co. machen es klar.


A riddle regarding type safety

Of course, I have explained to the students in my language theory class what 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


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