A few questions

[Timon Gehr]

On 07/29/2012 06:24 PM, bearophile wrote:
> 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?
>

Google for "freedom before commitment". The example is in the paper.
Apparently the unsoundness was recently fixed though -- the faulty
assignment in question is now correctly rejected by the online Spec#
compiler.