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