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

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Mon, 13 May 2013 22:01:56 -0500, Randy Brukardt wrote:

> "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.

You are saying that there are political reasons not to do this. I am fully
aware of this. I am not a politician and have not idea how to deal with
that. My point is that these reasons are NOT technical ones.

You suggest that there could be a way to convince people like you by
presenting some formalism? Seriously? You would reject the formalism using
same methods you and others did before. We could not even agree on the
notion of type! Not even on IMPROTANCE of types for Ada!

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de