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.
