A few questions

[Timon Gehr]

On 07/27/2012 04:35 PM, bearophile wrote:
>
> But implementing good non-null types in library code is hard

It is closer to impossible than to hard.

> (rather harder than implementing vector ops in library code on library defined
> vectors). I think @disable isn't enough to cover what Spec# shows good
> non-null types are meant to be.
>

Non-null types in Spec# are unsound.