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!.POSTED!not-for-mail From: Paul Rubin Newsgroups: comp.lang.ada Subject: Re: Ada Distilled by Richard Riehle Date: Fri, 27 Jul 2018 13:35:19 -0700 Organization: A noiseless patient Spider Message-ID: <87muuce7so.fsf@nightsong.com> References: <72ccb7fa-a9cb-42e6-8c29-3c06da281a45@googlegroups.com> <2212eb54-cb4a-446f-9cdf-287ef220e2c2@googlegroups.com> <1b5a58b2-65b7-4df8-80b5-03e208d249e1@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: reader02.eternal-september.org; posting-host="465eefdafb258f2581187c15f86634f1"; logging-data="16435"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX184PUixcAtadYqXIe9jsIBr" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux) Cancel-Lock: sha1:wylFiM8VUB4jn8LZ8nyfgV70g5s= sha1:ioUZZtgct597G9u7NSJMnS9/uh0= Xref: reader02.eternal-september.org comp.lang.ada:53986 Date: 2018-07-27T13:35:19-07:00 List-Id: "Dan'l Miller" writes: > Conversely, if Ada'Succ or Ada++ or AdaNG or hypoAda/Ada/hyperAda (or > whatever its name would be) would embrace overt set operations* over > the sets of types, subtypes, class-trees, and so forth at either > compile-time or run-time or both, now that might lead to an > interesting destination of super-dooper Ada++ doing something special > & useful that no** other language can do, including current Ada. Doing those sorts of checks at runtime is not too bad and you can specify signatures like that for runtime checking with Ruby's contracts gem. You can also specify them for the Erlang Dialyzer, which does static checks but which is intentionally unsound ("success typing"). That is necessary because of Erlang's runtime typing and the body of existing code that relies on it. It lets some errors through to avoid reporting false positives. I've used both of these and they work, though Ruby contracts can impose a lot of runtime overhead if you use them carelessly. Example: if you have a function whose contract says its input is an array of widgets, Ruby's contract checker has to scan the array (which could have a million elements) to make sure that each element is in fact a widget. I think for Ada, for that level of precision and given that Ada wants to be statically checked to the extent possible, you probably want SPARK rather than stuff in the type system. You really do need a theorem prover once the types get that complicated. But, once you're ok with that, you can encode anything in types. That's how Coq works, and similarly Agda, Idris, etc. SPARK is probably more in Ada's spirit. Links: Ruby contracts: https://github.com/egonSchiele/contracts.ruby Erlang Dialyzer: http://erlang.org/doc/man/dialyzer.html Idris example: https://www.idris-lang.org/example/