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:a30a:: with SMTP id m10-v6mr20164045ioe.28.1525660213431; Sun, 06 May 2018 19:30:13 -0700 (PDT) X-Received: by 2002:a24:d34a:: with SMTP id n71-v6mr33151itg.5.1525660213242; Sun, 06 May 2018 19:30:13 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.linkpendium.com!news.linkpendium.com!news.snarked.org!border2.nntp.dca1.giganews.com!nntp.giganews.com!u74-v6no2543414itb.0!news-out.google.com!f20-v6ni1013itd.0!nntp.google.com!v8-v6no3679072itc.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sun, 6 May 2018 19:30:12 -0700 (PDT) In-Reply-To: <7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.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: <7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: Why not Coq2Ada program extraction? From: "Dan'l Miller" Injection-Date: Mon, 07 May 2018 02:30:13 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Xref: reader02.eternal-september.org comp.lang.ada:52056 Date: 2018-05-06T19:30:12-07:00 List-Id: On Monday, April 30, 2018 at 10:38:13 PM UTC-5, Dan'l Miller wrote: > For a rather lucid tutorial on Coq as applied to correctness proofs of pr= ograms, please see the online editions of the 3-volume set of books: >=20 > https://SoftwareFoundations.cis.upenn.edu Over on =E2=80=9CHow to get Ada to =E2=80=98Cross the chasm=E2=80=99?=E2=80= =9D top-level posting on Sunday, April 29, 2018 at 1:52:41 PM UTC-5, Paul R= ubin wrote: > This book is good: http://www.cs.cmu.edu/~rwh/pfpl.html >=20 > So is this: https://softwarefoundations.cis.upenn.edu/ One potential answer to the OP's question of =E2=80=9CWhy not Coq2Ada progr= am extraction?=E2=80=9D could be: because perhaps Coq isn't the best* (or = only) tool for the job. Perhaps HOL4 or HOL-omega is instead a more access= ible tool for people who grok symbolic logic but don't grok that weird CoC = school of thought, pursuant to a hol2ada (to add Ada to its current reperto= ire of standard ML, Scala, Haskell, and OCaml). * Coq is based on the weird idea of calculus of constructions (CoC) instead= of logic. This at times leads to odd/scary observations, such as Coq succ= essfully =E2=80=9Cproving=E2=80=9D what would clearly be an axiom in some o= ther approaches. Bing or Google search for setting Coq on a different axio= m system, and you will find the results quite spartan. But perform that sa= me search against HOL, and all sorts of setting HOL on a different axiomati= c system show up: HOL-TLA, HOL-omega, HOL-ZF, and so forth. As it turns out Coq isn't the only one to have made progress in program-ver= ification-based/proof-based decompilation/reverse-engineering of machine co= de. Isabelle/HOL (i.e., HOL4, based on more-recognizable[-to-people-who've= -studied-symbolic-logic] garden-variety higher-order logic) is at somewhat = the same era of progress on that topic of producing interesting results tak= ing machine-code on a variety of ISAs as input: https://acjf3.github.io//papers/itp15.pdf If any of these theorem-proving-based tools can be applied to arbitrary(?) = machine code of each mainstream ISA, then at some (perhaps na=C3=AFve) leve= l, it would seem to be applicable to arbitrary 3GLs such as Ada as well (vi= a perhaps the same technique of Hoare triples). Or at least that's my stor= y and I am sticking to it. ;^) If you asking yourself, =E2=80=9CI want to be a proof engineer; what is a w= ay that I can make that happen?=E2=80=9D The following WWWpage is the Isabelle/HOL (based on standard ML) answer, mo= re than the Coq (based on OCaml) answer. (Eventually, I suspect that there= will be more of an Ada-esque answer during the 2020s, but we need to start= somewhere from whence to borrow ideas.) https://proofcraft.org/blog/proof-engineer-reading.html Isabelle/HOL (i.e., HOL4) http://isabelle.in.tum.de Or if you insist on working on code generators of Ada source code (e.g., fo= r multistage programming, which seems to be required in some variant to sol= ve the Ada-to-OS binding problems that Ada-WinRT is solving and that C++/Wi= nRT & Embeddinator-4000 is solving for other langauages), there is an exten= sion of HOL4 to omega lambdas: HOL-omega. http://www.trustworthytools.com/id17.html What is that System F and omega stuff? (System F is generally in the ballp= ark of what Ada calls generics [compile-time polymorphism] and tagged recor= ds [run-time polymorphism]. Omega is generally in the ballpark of code gen= erators of Ada generics and code generators of Ada tagged records.) System= F and System F-sub-omega are vertices on the Barendregt lambda cube (or si= des the Barendregt octahedron, if you prefer), which is a coordinate system= of sorts of how expressive, say, a programming language is regarding types= , values, and their interplay: https://en.wikipedia.org/wiki/Lambda_cube AIUI, Ada is capable of System F-sub-< (i.e., shorthand for System F for th= e tree of polymorphic OO subtypes, which Ada calls 'Class) via tagged types= at run-time and System F via parameterized types at compile-time. Modern = C++2017 is capable of those two plus much of System F-sub-omega via its klu= dgey Turing-complete parameterized-type specializations. (I am still slowl= y investigating just how aware Rust's macro language is of Rust's types; if= Rust's macro language is quite intimately aware to the point of reflection= upon types declared so far and synthesis of fresh types in reaction to typ= es declared so far, then Rust's macro language might be System F-sub-omega = as well.) Some source-code generators for Ada might achieve System F-sub-o= mega as well, if they can synthesize and modify type declarations to be emi= tted in the generated Ada source code; Ada-WinRT and C++/WinRT and WinRT-Ru= st all have some degree of capability in this space in reflecting upon DLLs= & their .winMD files that effectively act as a reflection mechanism upon t= he DLL in Microsoft Windows 8, 8.1, & 10 world, so that COM/ATL types in .w= inMD/DLL-land get massaged into Ada, C++, and Rust types, respectively.