July 28, 2012
> Huh? I believe you have misunderstood something here. The struct is a form
> of smart pointer. It behaves like a pointer does, and lets you have
> polymorphism, inheritance and all that stuff that comes with classes.
> Granted, I have found a few issues with the version I posted (mostly to do
> with subclassing). Most have been fixed in this version, but some are
> unfixable until issue 1528 has been resolved.

Some kind of smart pointer is easy to write, or not?
What's wrong with this?
http://dpaste.dzfl.pl/11a4d692
July 29, 2012
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.
July 29, 2012
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
July 29, 2012
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.

1 2 3 4 5
Next ›   Last »