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 X-Received: by 2002:a6b:1f14:: with SMTP id f20-v6mr3456587iof.8.1524149310543; Thu, 19 Apr 2018 07:48:30 -0700 (PDT) X-Received: by 2002:a9d:5888:: with SMTP id x8-v6mr396605otg.0.1524149309995; Thu, 19 Apr 2018 07:48:29 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!feeder.erje.net!2.eu.feeder.erje.net!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!f63-v6no415252itc.0!news-out.google.com!15-v6ni674itg.0!nntp.google.com!k65-v6no411656ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Thu, 19 Apr 2018 07:48:29 -0700 (PDT) In-Reply-To: <87h8o7lowg.fsf@nightsong.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=47.185.233.194; posting-account=zwxLlwoAAAChLBU7oraRzNDnqQYkYbpo NNTP-Posting-Host: 47.185.233.194 References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <878t9nemrl.fsf@nightsong.com> <87h8o7lowg.fsf@nightsong.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: =?UTF-8?B?UmU6IEhvdyB0byBnZXQgQWRhIHRvIOKAnGNyb3NzIHRoZSBjaGFzbeKAnT8=?= From: "Dan'l Miller" Injection-Date: Thu, 19 Apr 2018 14:48:30 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 4292 X-Received-Body-CRC: 2366975960 Xref: reader02.eternal-september.org comp.lang.ada:51632 Date: 2018-04-19T07:48:29-07:00 List-Id: On Thursday, April 19, 2018 at 12:57:07 AM UTC-5, Paul Rubin wrote: > "Dan'l Miller" writes: > > Coq-esque and Zed-notation-esque systems of logic need to be the > > future of Ada. >=20 > ... > Coq is based on constructive type theory (CTT) which is more usually > associated with functional programming than imperative programming. It > can be used to prove theorems about imperative programs, but also, Coq > itself can be seen as an ML dialect with super-precise types. For > example, the CompCert verified C compiler (compcert.inria.fr) is written > in Coq. Yes, that is true, but the Coq community has been pushing Coq far beyond = its origins in CTT & derivational-type theory for merely functional program= ming. Coq is increasingly setting its sights on the wild-west worlds of C = and machine code: http://plv.csail.mit.edu/bedrock https://www.lri.fr/~paulin/LASER/course-notes.pdf https://dl.acm.org/citation.cfm?doid=3D2676724.2693162 http://vst.cs.princeton.edu https://archive.org/details/CertifiedProgrammingWithDependentTypes https://galois.com/blog/2014/07/tech-talk-verifying-c-programs-coq-using-vs= t https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-= assembler/?from=3Dhttp%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople= %2Fnick%2Fcoqasm.pdf http://www.cl.cam.ac.uk/%7Epes20/pip2014-slides/PiP2014.pdf > Z-notation is used to specify the behaviour of a program, which is then > verified using external tools like SPARK using state transformer logic > (Hoare triples, separation logic, etc). I bring up Z-notation as a relatively-widely-known example of logic-based s= ystem-specification language to the Ada community because I find it extraor= dinarily odd that on one hand Ada seeks to be the safety language for criti= cal systems (OMG! we're all gonna die without Ada), but then on the other h= and defines Ada's language semantics in English prose that compiler vendors= cannot take as direct input into their compiler implementations. (And the= n the Ada community argues for decades on end here at comp.lang.ada whether= this darned compiler versus my exemplary program versus the ARM/AARM got i= t wrong regarding some unexpected Ada behavior, when a nontrivial fraction = of these debates have the unverified-incompleteness* of or the ambiguity of= English prose in the ARM as the root cause.) * Oops, the ARG forgot to handle that case, which might have been easily ca= ught under formal-methods analysis of a non-prose specification of Ada's se= mantics. Speaking of SPARK, here is SPARK-esque analogue for a subset of C++: http://EscherTech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf http://EscherTech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.ppt Btw, Luke Guest, your envisioned out-with-the-cruft-&-in-with-the-well-oile= d-machine Ada for the 21st century would not have its language specificatio= n in English prose.