bearophile wrote:
Anyway, the topic of this whole tread is about non-nullable types in D,
I read your first post as arguing that Spec# in general was a language well designed for security - "Spec# looks very well designed and thought out"
copying from the very good implementation of Spec# (with the little changes I have shown). Walter, instead of poking and teasing me as a ten year old does, why we don't start talking about serious things?
Given the store you've set by integer overflow detection, sorry, I couldn't resist teasing you about Spec# failing at that.