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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.36.77.142 with SMTP id l136mr777397itb.12.1494780364903; Sun, 14 May 2017 09:46:04 -0700 (PDT) X-Received: by 10.157.82.15 with SMTP id e15mr41172oth.6.1494780364871; Sun, 14 May 2017 09:46:04 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.unit0.net!takemy.news.telefonica.de!telefonica.de!ecngs!feeder2.ecngs.de!feeder.usenetexpress.com!feeder1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!border2.nntp.dca1.giganews.com!nntp.giganews.com!c26no1444330itd.0!news-out.google.com!v18ni2417ita.0!nntp.google.com!c26no1440370itd.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sun, 14 May 2017 09:46:04 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=73.91.216.22; posting-account=viu8XwoAAAAzhf3NstShw2l2R6SQaaQR NNTP-Posting-Host: 73.91.216.22 References: User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <1c0e2c7c-4fd6-43d1-9848-f03e1a72bcb3@googlegroups.com> Subject: Re: Rust's temporal safety for Ada/SPARK From: digitalkevlar@gmail.com Injection-Date: Sun, 14 May 2017 16:46:04 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:46777 Date: 2017-05-14T09:46:04-07:00 List-Id: @ Robert Eachus "There are some cases that require run-time checking, and most programmers = consider code that needs run-time checking as a bug" I can see why they'd avoid such constructions if their tooling couldn't pro= ve them safe. If another tool can, though, then I'm thinking it's a bug in = Ada in that Ada's model or tools can't handle that analysis at compile-time= . Something worth fixing with R&D. That's why I'm trying to assess what Ada= can do currently in this area. Several other languages knock this problem = out at compile time. They're functional, logical, and imperative. So, I kno= w it is feasible in general case. @ All Niklas Holsti's post shows he understands what capability I'm describing. R= ust code can be shown free of double-free's and dangling-pointers at *compi= le-time* with *no runtime checks or GC*. It does it with just a few simple = rules. Here's the simplest, shortest description I could find to save you a= ll time: https://stackoverflow.com/questions/36136201/how-does-rust-guarantee-memory= -safety-and-prevent-segfaults Those are combined with "traits"... or something else in language... to all= ow race-free concurrency. Instead of mandating one model for language, vari= ous models of concurrency are defined in libraries to let you use model eas= iest for your problem. Language's ownership model & borrow-checker ensures = they're all memory-safe and race-free along with any code using them. So, y= ou get these guarantees even in multi-threaded code doing many allocations = and de-allocations of memory dynamically. New developers do have a hard tim= e fighting with the borrow-checker early on. My meta-analysis of their comm= ents indicates much of it is intrinsic to safely handling ownership and bor= rowing of references that C and GC'd languages didn't teach them. The tool = just enforces rules (i.e. affine types) known to work. Learning curve is ab= out 1-2 months of practice until they say borrow-checker rarely has problem= s with their code. So, can someone today use Ada in a straight-forward way to write single- or= multi-threaded applications that are, in every use-case, totally immune at= compile-time to use-after-free and double-free errors with zero, runtime o= verhead? Or can it not do that?