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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Thu, 15 Dec 2016 09:41:48 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32840 Date: 2016-12-15T09:41:48+01:00 List-Id: On 14/12/2016 22:46, Shark8 wrote: > On Wednesday, December 14, 2016 at 1:04:53 PM UTC-7, Dmitry A. Kazakov wrote: > It's relevant because it is exactly showing how to represent > restrictions [exclusions] on values (within a set); and, as we know, a > type is a set of values and a set of operations acting on those values. > -- This maps directly to Ada, given the LRM's definition of subtypes. Well, but first it is an implementation issue, as such, of a very secondary order to the question of constrained types and other means to create new types. Secondly arbitrary constraints is low level and thus a bad idea to introduce into the type system, as dynamic predicates promptly illustrate. Resemblance to Ada 83 subtypes is only superficial. >>> In this light, integrating SPARK proving with the Ada compiler could >>> allow for better optimizations... and if it can be done in such a way >>> that it can be leveraged in other portions of the compiler (say semantic >>> checks), then why not use it? >> >> When that comes into life, programmers surely will, though not in the >> form of preconditions, because as I said, it is bad design. The rule is >> weakening preconditions, strengthening post-conditions. > > I think you may be overestimating the group "programmers". > Seriously, the thread "C# new features (v.7)" -- > https://groups.google.com/forum/#!topic/comp.lang.ada/mLZIo_Sjm5c -- > lists things that "modern" languages are just getting that Ada has had > for years. Ada programmers? Ada people are very interested in formal verification. The problem is integration of SPARK into Ada and arbitrary constraints would be only obstacle here. The lower is the level of a construct more difficult is verification. > Integrating these useful technologies into the compiler in a manner > that is invisible to users [non-implementer Ada programmers] is a good > way to ensure that the tools are used. (e.g. the Ada compiler does > automatically what C's Lint did, and is much better for it. [Most of the > C programmers I knew in college *never* used lint.]) Right, because it is a tool you could use or not. In Ada type declarations must be there, so it is not a tool, but an integral part of the language. This is why "pre"-aspects is a non-starter even ignoring their semantic consistency issues. You can do things with or without them. Psychologically it won't work. > Now, if we can also leverage these technologies to make > implementations [of Ada] better [quality-wise] and more maintainable, > then that's win-win all the way around at the cost of (a) designing your > IR to be amiable to the prover-module, and (b) implementing the > prover-module. I am against that, see above, it must be an integral part of the Ada's declarative framework, never a module or a tool. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de