From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on ip-172-31-74-118.ec2.internal X-Spam-Level: X-Spam-Status: No, score=-0.9 required=3.0 tests=BAYES_00,XPRIO autolearn=no autolearn_force=no version=3.4.6 Path: eternal-september.org!reader02.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED.rrsoftware.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Adacore joins with Ferrous Systems to support Rust Date: Thu, 3 Feb 2022 21:38:16 -0600 Organization: JSA Research & Innovation Message-ID: References: <87o83pzlvm.fsf@nightsong.com> <87bkzpyqx3.fsf@nightsong.com> <8735l0zo6j.fsf@nightsong.com> <87v8xwy3y7.fsf@nightsong.com> Injection-Date: Fri, 4 Feb 2022 03:38:17 -0000 (UTC) Injection-Info: franka.jacob-sparre.dk; posting-host="rrsoftware.com:24.196.82.226"; logging-data="26052"; mail-complaints-to="news@jacob-sparre.dk" X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.7246 Xref: reader02.eternal-september.org comp.lang.ada:63470 List-Id: "Paul Rubin" wrote in message news:87v8xwy3y7.fsf@nightsong.com... ... > Well are you familiar with red-black trees? They are a data structure > similar to B-trees which you may have seen. Basically the trees have > nodes that are coloured either red or black, and there are some rules > such as that internal red nodes can have only black children, and that > enforces some invariants that keep the trees balanced so that lookups > and updates are guaranteed to run fairly fast. > > Now these trees have been implemented in many languages, and if you look > at almost any implementation, there is usually a test suite or internal > debugging code to make sure that the invariants are preserved after > doing an update. It is quite easy to make a mistake after all. But the > Haskell code doesn't have those tests. Why not? Because the invariants > are enforced by the datatype! If you make a mistake and mess up an > invariant, your code won't compile! It's the difference between > checking a subscript at runtime, and verifying that it in range with > SPARK. SPARK lets you get rid of the runtime check. Haskell's type > system is able to do similar things. Cool, and most likely useless. OOP is like that in many ways, it lets you make a bunch of static checks, but to get them, you have to contort your design in awful ways. And then it is hard to extend, as you have a huge number of routines to override to get anything done. I'm convinced that the answer (as much as there is an answer -- always beware of anyone bearing silver bullets ;-) is in the quality of tools (and language implementations). In any language with dynamic checks, one can easily reduce the problem of correctness down to simply proving that no check fails. So the question is how one can accomplish that with the least complication for the actual programmer. Janus/Ada has a switch that can give you a warning for any implicit check that remains in the code after optimization. Combine that with the warnings-as-errors switch, and no program that could have a (detectable) bug can compile. Moreover, in Ada at least, one can introduce essentially any condition that you want to know as some form of assertion. To take your red-black example. In Ada, I'd model the tree as a single type with two subtypes, with Red and Black predicates that enforce the conditions. Then, using the switches mentioned above, you could only compile the program if the compiler can eliminate the condition checks (it should be able to, if they are really complete). The problem with this scheme, of course, is the quality of the implementation in terms of eliminating unneeded checks. For now, Janus/Ada can only do this sort of elimination inside of an extended basic block, and if something prevents a subprogram from being converted to a single extended basic block, you're likely to get spurious warnings. (And it only implements advanced elimination on a few kinds of checks, enough to prove the concept but not enough to be practical.) The key for a programming language design is to minimize what Ada calls erroneous execution (undefined behavior), because it is that possibility which stop proofs in their tracks (or at least should; at least some tools ignore that possibility and essentially give garbage results as a consequence). Ada needs work in that area, but most other languages need more -- Ada at least detects most problems with dynamic checks. Anyway, that's my 20 cents (inflation, you know). :-) Randy.