Re: Why not Coq2Ada program extraction?

["Dan'l Miller" <optikos@verizon.net>]

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 programs, please see the online editions of the 3-volume set of books:
> 
> https://SoftwareFoundations.cis.upenn.edu

Over on “How to get Ada to ‘Cross the chasm’?” top-level posting on Sunday, April 29, 2018 at 1:52:41 PM UTC-5, Paul Rubin wrote:
> This book is good: http://www.cs.cmu.edu/~rwh/pfpl.html
> 
> So is this: https://softwarefoundations.cis.upenn.edu/

One potential answer to the OP's question of “Why not Coq2Ada program extraction?” could be:  because perhaps Coq isn't the best* (or only) tool for the job.  Perhaps HOL4 or HOL-omega is instead a more accessible 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 repertoire 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 successfully “proving” what would clearly be an axiom in some other approaches.  Bing or Google search for setting Coq on a different axiom system, and you will find the results quite spartan.  But perform that same search against HOL, and all sorts of setting HOL on a different axiomatic 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-verification-based/proof-based decompilation/reverse-engineering of machine code.  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 taking 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ïve) level, it would seem to be applicable to arbitrary 3GLs such as Ada as well (via perhaps the same technique of Hoare triples).  Or at least that's my story and I am sticking to it.  ;^)

If you asking yourself, “I want to be a proof engineer; what is a way that I can make that happen?”
The following WWWpage is the Isabelle/HOL (based on standard ML) answer, more 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., for multistage programming, which seems to be required in some variant to solve the Ada-to-OS binding problems that Ada-WinRT is solving and that C++/WinRT & Embeddinator-4000 is solving for other langauages), there is an extension 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 ballpark of what Ada calls generics [compile-time polymorphism] and tagged records [run-time polymorphism].  Omega is generally in the ballpark of code generators 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 sides 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 the 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 kludgey Turing-complete parameterized-type specializations.  (I am still slowly 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 types 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-omega as well, if they can synthesize and modify type declarations to be emitted in the generated Ada source code; Ada-WinRT and C++/WinRT and WinRT-Rust all have some degree of capability in this space in reflecting upon DLLs & their .winMD files that effectively act as a reflection mechanism upon the DLL in Microsoft Windows 8, 8.1, & 10 world, so that COM/ATL types in .winMD/DLL-land get massaged into Ada, C++, and Rust types, respectively.