From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Text_IO, was: Re: Something I don't understand Date: Thu, 20 Feb 2014 22:45:26 +0200 Organization: Tidorum Ltd Message-ID: References: <4a3e55f6-9f54-4084-9f37-96efd4b0d349@googlegroups.com> <0b358700-871b-4603-addd-65e07c7d59e5@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: individual.net QBwE+IOncXdYiBzc0XeHGwf5pYvJ5hsLcT+FsfSOQHUsQzlH0c Cancel-Lock: sha1:+WERHs6jZETNehHYTtcXo3iuBLE= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:24.0) Gecko/20100101 Thunderbird/24.3.0 In-Reply-To: Xref: news.eternal-september.org comp.lang.ada:18712 Date: 2014-02-20T22:45:26+02:00 List-Id: On 14-02-20 00:01 , Robert A Duff wrote: > Niklas Holsti 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 . @ .