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: Rust's temporal safety for Ada/SPARK Date: Sun, 14 May 2017 19:18:45 +0200 Organization: Aioe.org NNTP Server Message-ID: References: <1c0e2c7c-4fd6-43d1-9848-f03e1a72bcb3@googlegroups.com> NNTP-Posting-Host: BYuA7L7MRjuLLjcoGHOBxw.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 10.0; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.1.0 X-Notice: Filtered by postfilter v. 0.8.2 Content-Language: en-US Xref: news.eternal-september.org comp.lang.ada:46778 Date: 2017-05-14T19:18:45+02:00 List-Id: On 2017-05-14 18:46, digitalkevlar@gmail.com wrote: > Niklas Holsti's post shows he understands what capability I'm > describing. Rust code can be shown free of double-free's and > dangling-pointers at *compile-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 all time: > > https://stackoverflow.com/questions/36136201/how-does-rust-guarantee-memory-safety-and-prevent-segfaults Helpful would be to have an example where pointers are needed. The example provided requires no pointers. So in Ada case, no such problem exist at all. [...] > 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 overhead? Or can it not do that? Without having other examples, the answer is: there is no such problem in Ada because arguments of task rendezvous are not pointers. For multitasking, problems arise when the method of problem decomposition requires constructs which are not safe in the sense that safety is statically undecidable. Which means that a decidable static constraints would simply kill the algorithm. From the practical perspective it is usually possible to trade one danger for another (lesser, greater, equal), e.g. to exchange deadlock for livelock, but not getting rid of it altogether. Considering the problem of having tasking safe per construction, my impression is that constraints are no or very little help. Additional methods of decomposition are. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de