Hello bearophile,
BCS:
My take on this is that the type system should promise to check
something and then always check it or say nothing at all. It should
never say maybe. The worst it can do is check something most of the
time but then not check it in the really hard cases (where I most
need it).
I am not sure.
Type systems are like automatic systems that perform a proof. Goedel
told us that in some cases there's no way to decide if something is
true. This happens for type systems too, and the more complex type
systems are, the more situations there are where they reach blocking
situations.
All real programs contain many bugs, so you have think about finding
bugs as a probabilistic effort, your purpose is to reduce some
probabilities, because in real-world programs you can't hope to catch
all bugs. There is not much difference if some of those bugs come from
bugs in the type system, in the compiler, in the program, etc. In C#
the type system gives you errors for uninitialized variables, this is
a very useful feature that I'd like in D too, but there are situations
where such static analysis fails, and the C# compiler gives you false
positives.
You want a reliable type state that gives zero false negatives, this
may be possible, I don't know, but it has a cost, because it has to
turn some undetermined cases into false positives. Maybe there is no
way to design a typestate as you desire in D.
I have no problem with tools that do what you are looking for. That said
I have major problems with that being the type system. The type system should
be defined in terms of "MUST", "MUST NOT", "REQUIRED", "SHALL" and "SHALL
NOT" and should never use the term, "SHOULD", "SHOULD NOT", "RECOMMENDED",
"MAY", and "OPTIONAL"
http://www.faqs.org/rfcs/rfc2119.html
To do that with the type of static analyses you want would requiter specifying
the algorithms to be used and that would be pointless as they would be out
of date within months.
--
... <IXOYE><
