Re: Text_IO, was: Re: Something I don't understand

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 14-02-20 00:01 , Robert A Duff wrote:
> Niklas Holsti <niklas.holsti@tidorum.invalid> writes:
> 
>> No, dynamic type safety is not fully "Ada type safe". Ada is (mainly)
>> statically type safe; dynamism only enters in subtype safety.
> 
> Well, if you take the view that "types" are "those things that can be
> checked statically", then all programming languages are statically type
> safe, rendering the notion meaningless. 

Type safety to me means that code reading a datum interprets the datum's
representation correctly, using the same type/representation as the code
that wrote the datum. The value read is the value written, not some
unpredictable reinterpretation of the bits in memory.

This notion has nothing to do with what is statically checked or not
checked, and even less with what *can* be checked statically. Type
safety could be implemented by dynamically tagging each datum with its
type and checking tags at run time.

But "Ada type safety" to me means that type safety is checked
statically. Perhaps I am being too pedantic and strict about this, but I
think I'm not alone in this view.

> In other words, the term "subtype" in Ada is a cheat, deliberately used
> to enable bogus claims about static type safety in Ada, as if the
> run-time checks associated with subtypes somehow don't count.

Subtype checking deals with permitted values, not with correct use of
the machine representation. I don't see any cheating, it is well
understood that such constraints or assertions on values need run-time
checks, although more and more of them can also be proved with SPARK or
other such tools.

Consequently, when I program in Ada, and subprogram Foo signals a
Constraint_Error because its parameter X (type Integer) has the value
105, while the subtype of X permits only 1..10, I can be sure that the
caller of Foo really provided the parameter value 105 (type Integer). I
don't need to worry that the caller provided a Float parameter which Foo
tried to interpret as Integer.

Simon's proposal for printf-like formatting in Ada is not, IMO, "Ada
type safe", because it needs a run-time check to verify that the type of
a parameter is correct, and this is because the correct type depends on
the *value* of the format string. But I admit that one can take the
other view, that the type of the parameter is always correct, and any
run-time problems are "subtype" errors in the value of the format string.

Clearly, however, Simon's proposal (and any proposal that depends on a
potentially dynamic format or template value) reduces the level of
static type checking, which IMO is bad.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
      .      @       .