[contest] Is a Cow an animal ++

[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 within months.

Are you talking about the specification of the type system here? 
Denotational semantics? Operational semantics? That rfc has nothing to do 
with type systems, now does it.