From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.5-pre1 (2020-06-20) on ip-172-31-74-118.ec2.internal X-Spam-Level: X-Spam-Status: No, score=0.0 required=3.0 tests=BAYES_40,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.5-pre1 X-Received: by 2002:ac8:1626:: with SMTP id p35mr10169qtj.326.1601327168296; Mon, 28 Sep 2020 14:06:08 -0700 (PDT) X-Received: by 2002:a37:a750:: with SMTP id q77mr1274047qke.377.1601327168099; Mon, 28 Sep 2020 14:06:08 -0700 (PDT) Path: eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.gegeweb.eu!gegeweb.org!usenet-fr.net!proxad.net!feeder1-2.proxad.net!209.85.160.216.MISMATCH!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Mon, 28 Sep 2020 14:06:07 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: google-groups.googlegroups.com; posting-host=146.5.2.231; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 146.5.2.231 References: <00cd3aaa-d518-43a2-b321-58d6fae70aebo@googlegroups.com> <57eb7a65-51ea-4624-b9dc-9c4dda0fee59n@googlegroups.com> <5f70fd3b$0$13541$426a74cc@news.free.fr> <76af9bfd-e0f3-4620-83b5-779374fe5859n@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <61263279-e55c-4cd8-97a5-7c222136b45cn@googlegroups.com> Subject: Re: is there a version of unix written in Ada From: Shark8 Injection-Date: Mon, 28 Sep 2020 21:06:08 +0000 Content-Type: text/plain; charset="UTF-8" Xref: reader02.eternal-september.org comp.lang.ada:60326 List-Id: On Monday, September 28, 2020 at 2:30:25 PM UTC-6, Dmitry A. Kazakov wrote: > > There are reasons why low-level C rules the API. Higher-level interfaces > are incredibly fragile. I believe SPARK is the way, but I have no idea > where to start. I'd imagine with a system like this: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.26.2533&rep=rep1&type=pdf but integrating passing SPARK-proofs into the upward-merge operation. > > Personally, I think a Github readme.md page would be ideal at first as people could contribute ideas, complements but still be managed. (pull request, approve, revise etc) > The problem is that all such projects tend to die due to lack of interest. I could do this.