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:1wzphazeho17m$.zy00zh7l7yu5$.dlg@40tude.net...
> On Mon, 13 May 2013 22:01:56 -0500, Randy Brukardt wrote:
...
>> 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.

Two points here:

(1) Virtually all constraints are political, not technical. Without the 
constraints posed by cost, compatibility, and the like, essentially anything 
is possible. Especially in software. One of the first problems we had to 
solve when starting as one of the Ada 9x User-Implementer teams was how to 
answer the question of implementability that we were supposed to provide 
feedback on. Virtually everything is implementable with enough effort (and 
levels of indirection); the question was where to draw the line. Eventually, 
we found that the question had been posed incorrectly; the Ada 9x team 
wanted to know about any implementation difficulties so they could sort out 
whether or not to change the feature to reduce the issues.

Indeed, you could consider Ada's goals like readability and maintainability 
to be political, rather than technical, constraints. So pretty much anything 
that could be proposed is going to have to deal with the various political 
constraints -- they *cannot* be ignored in any real-world scenario.

I'm not a politician either, and I'd rather avoid those sorts of games, but 
one has to do what it takes to get things done.

> 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!

You might be right. The only sure-fire way to convince everyone would be to 
write wording for the entire proposal and as well have a prototype 
implementation. If the prototype implementation were to show only minor 
incompatibilities when processing existing Ada code (including the ACATS, 
AdaCore test suite, and the like), that would be clear evidence that it is 
OK.

But I'm quite aware that that's impractical. (Which is the crux of the 
problem, of course.)

I suspect that you might be able to convince some people if you provided a 
fully fleshed out proposal with revisions to the wording of the Standard. 
That would mitigate the terminology problem because you would have to 
provide definitions for all of the terms that you use. But I suspect that it 
also too large a job for one person (as someone who has undertook smaller 
revisions that took a *long* time, like the revisions to support the aspect 
terminology -- and the language has long had some of that terminology, I 
wasn't quite starting from scratch.)

When I was talking about a semi-formal proof above, I was thinking of it 
layered on top of fully fleshed out wording. I don't think you're every 
going to get much interest without that, precisely because of the issues 
with terminology.

                                      Randy.