Hello retard,
Fri, 01 Oct 2010 03:18:29 +0000, BCS wrote:
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 withihe n months.
Are you talking about the specification of the type system here?
Denotational semantics? Operational semantics?
Any and all of the above plus any less formal description of what the type
system must accept and reject.
That rfc has nothing to do with type systems, now does it.
Nope it doesn't, but it has everything to do with how those terms I used
are used in standards documents.
--
... <IXOYE><
