Re: MI is sloppy

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:43lprrmyik2q.1esp72deqcw6o.dlg@40tude.net...
> On Fri, 12 Dec 2008 13:15:35 +0100, Georg Bauhaus wrote:
>
>> Dmitry A. Kazakov schrieb:
>>
>>>> If you have an ambitious compiler, it might reach out,
>>>> at compile time, for objects whose behavior is then known
>>>> to be constrained by membership in a then known specific
>>>> subtype.
>>>
>>> ... and then inline raising Constraint_Error. Great!

For some reason, I didn't get the other messages to this thread.

But that's not what I'm suggesting. First of all, this is a contract 
failure; it has it's own dedicated exception (maybe Assertion_Error). In 
addition, I think compilers should be allowed to reject any program in which 
that it can be determined statically that the contract exception will 
unconditionally be raised. What a programming language can't do is mandate 
the cases in which that detection will occur. That will depend on the tools 
you use; a really good tool should be able to detect just about everything 
statically. (In addition, you could use an exception contract to force this, 
or the program would also be illegal.)

...
>> Deriving another type, even if not sufficiently different
>> from the original to warrant a type, is another formal
>> way to trigger the same effect on the programmer, at compile
>> time: "There is something odd about your program".
>
> No, the effect is fundamentally different. The effect is that the program
> becomes illegal, it may not run.

That's exactly what is possible with the contracts that I'm suggesting. But 
it cannot be mandated; we have to leave to the tools vendors to describe 
what is possible to detect statically (after giving them the framework).

...
>> If we wanted more of the minor differences covered
>> by type hierarchies, we might end up with a Qi type
>> system... For Ada?
>
> 1. Qt is not a programming language.
>
> 2. There is no minor differences in terms of correctness. An incorrect
> program is incorrect.

You are definitely wrong about this, at least in a finite world. The cost to 
fix some technically incorrect programs (in manpower, performance, 
useability, etc.) is greater than the cost of the error occurring. Such 
programs might be technically incorrect, but they're practically correct. 
This the reason that we tolerate erroneousness in the language definition. 
And it's the reason that we use exception handlers.

> There is no *any* way to predict the effect of incorrectness.

That is surely not true. An Ada bounded error occurs in a program that is 
incorrect, but the effect of that incorrectness is strictly bounded.

                                Randy.