Spec#, nullables and more

[bearophile]

Walter Bright:

>  From what I recall of Eiffel, a considerably older language (1985), Spec#'s DbC 
> design is almost a direct copy.

I am not expert about Eiffel, but I have read several documents about Spec#, I have written about thirty little/snippets programs in it, and from what I've seen, Spec# implementation of DbC looks more refined, for all the main corner cases of an OOP language (all that stuff about aggregate objects, ownership, mutable/consistent/committed state for objects, peer groups, and all the relative details. I didn't remember all those things in Eiffel. And those things aren't useless) (but also a bit less flexible, because it's all designed to be statically verifiable).

Bye,
bearophile