Re: function Is_Open (File : File_Type) return Boolean; :Text_io

["G.B." <bauhaus@futureapps.invalid>]

On 30.10.15 17:20, Dmitry A. Kazakov wrote:
> On Fri, 30 Oct 2015 15:32:16 +0100, G.B. wrote:
>
>> On 30.10.15 09:39, Dmitry A. Kazakov wrote:
>>> The concern is safe design. If [program] B has bugs it cannot be
>>> relied on to determine if it has them.
>>
>> Uhm, so what?  Which kind of program is relied upon to determine
>> if it has bugs or not?
>
> A program that contains run-time checks for bugs.

I don't think anybody says that, nor does "contract based design",
not the part with "relying"! As is apparent from the Ada Rationale
("for debugging..."). As was apparent from some quoted paragraphs.

Also of interest is Hoare's idea of a SIMPLYFYING_ASSUMTION.
Which is to be used in some situations(!), but not in others.

>> OTOH, what if we can learn about potential bugs because we happen
>> to think that a failed expression has exactly that potential
>> for us?
>
> What kinds of answer do you expect?

If someone is assuming that programmers will always start their
thinking from something comprehensively correct, I expect his
answer to reflect this.
In other cases, the ones I consider more ordinary, decent
programming, I'd expect this:

"... needs to be assessed empirically."

> Positive of *what*?

Positive of what we now have learned may (not) be the desired outcome.
In some cases, that's too late. In many cases, we stop before rollout.
We might be stymied.

> You first need a workable (...) definition of a correct
> program

What makes you assume that a specific, formalistic definition of
a correct program is the workable one?

Except per the narrow situation-excluding circularity of
"work" = "operation":
Considering the most successful software companies on this
planet, while they do not profit from selling correct (formally,
somehow) programs(*), they still strive for local correctness.
(A program that was correct for Ariane IV was not correct(?) for
... Again, situations!)

So, I guess, one might poke fun at tests that make test runs
of programs fail because the test was failing, one might start
from world-excluding definitions that of necessity produce
a contradiction, or one might make jokes about programming
efforts that assume that sufficient formalization is possible.
All are justified, IMHO.

__
(*) Since, who would pay for updates?