Timon Gehr: > Non-null types in Spec# are unsound. Really? I didn't know it. Surely its non-null design looks quite refined and thought-out. But maybe as say it's not enough still. Do you have a link where it shows it's unsound? Thank you, bye, bearophile