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.
