Re: Seeking for papers about tagged types vs access to subprograms

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:bkozr3g5i0hk$.15qnfap6hrj20$.dlg@40tude.net...
> On Fri, 10 May 2013 19:09:12 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:1jc46ynzptlxm.1fafjhr8hlblq.dlg@40tude.net...
>>> On Thu, 9 May 2013 16:43:29 -0500, Randy Brukardt wrote:
>> ...
>>>> The problem is, when you do that, you'd have no way to determine 
>>>> whether
>>>> or not it is really compatible. (After all, there is no formal model 
>>>> for
>>>> Ada, and there never has been.) Ada's definition is just a mass of 
>>>> English
>>>> text, and replacing it by a different mass of English text leaves one 
>>>> no
>>>> practical way to prove compatibility.
>>>
>>> Why should I need it if no existing Ada compiler does that? It will be 
>>> as
>>> compatible as any existing Ada implementation is. There is no reason to
>>> require more than that, e.g. formal verification.
>>
>> Because there is no other way to tell. No one is going to implement it 
>> (or
>> put it into the Standard) unless they know that it is "at least as
>> compatible as an existing Ada implementation". You're going to have to 
>> prove
>> that somehow, and that proof is going to have to be at least semi-formal,
>> because it is going to have to be convincing. Handwaving in a forum like
>> this is not a convincing proof.
>
> You didn't answer the question. If it goes without a proof now, why can it
> continue so?

I'm afraid I don't understand your question, so I can't answer it directly. 
I can only repeat the situation:

You are proposing a complete overhaul of the model of types in Ada. You keep 
claiming that this overhaul would be compatible without a shred of proof 
that this is achievable. You would have to find *some* way to convince the 
Ada community that your revised model is in fact 100% compatible with the 
current model. A semi-formal proof would clearly be the best way to do that.

Remember that Ada is defined in English, and as such there is not currently 
a formal way to tell if we're staying compatible. As such, there is a great 
reluctance to make major changes to the text, because there is no way to 
find regression errors. Our experience has been that we introduce about as 
many serious bugs to the standard as we make changes to it, simply because 
we can't easily tell when we break things.

As such, there would have to be an amazingly serious problem that absolutely 
had to be fixed in Ada for us to consider any major change to the model --  
even if such a model would be an improvement. The only sure-fire way to get 
a level of confidence in such a model would be to provide extrodinary proof 
of its correctness compared to the existing standard. And that's all I'm 
talking about when I say a "semi-formal proof" is needed.

                                                Randy.