Why not Coq2Ada program extraction?

Why not Coq2Ada program extraction?

[Dan'l Miller]

Coq already extracts (generates) OCaml, Scheme, and Haskell from proofs.  Extracting Rust from Coq proofs is a work-in-progress at https://github.com/pirapira/coq2rust

Why hasn't anyone ever developed Ada extraction from Coq proofs?  Perhaps the coq2rust work-in-progress can serve as a guide and/or inspiration for an analogous coq2ada.

What if the entire English-prose ARM were re-written as Coq proofs?  Then a fresh new Ada compiler front-end could be extracted therefrom (and it would be provably verified as conforming to the ARM-in-translation-to-Coq, leaving only defects in the English prose and defects in the transliteration of prose to Coq and bugs in Coq and bugs in the Coq-to-Ada extraction as the remaining origins of compiler bugs).  Perhaps this is the eventual path to the disruptor to dislodge GNAT for which some have been yearning.

What if either the front-end's interface to LLVM or each ISA were re-written as Coq proofs?  Then a fresh new Ada compiler back-end could be extracted therefrom.

(Either all that or else it would pole-vault [Coq-extracted-]OCaml to being a language in which to implement Ada compilers.)

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

Re: Why not Coq2Ada program extraction?

[Paul Rubin]

"Dan'l Miller" <optikos@verizon.net> writes:
> Why hasn't anyone ever developed Ada extraction from Coq proofs?

That's interesting to hear about Rust.  Coq (like Ocaml, Scheme, and
Haskell) is lambda calculus once you look past the types, so extracting
to those languages is natural.  This gets back to our earlier
discussion: lambda calculus is a computational model equivalent to a
Turing machine, with unlimited memory.  You can translate the lambda
calculus computational part to actual machine code, but you end up
simulating the unlimited memory using garbage collection.  There's a
book about it here:

https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/

I wouldn't have thought it possible to extract to Coq a non-GC'd
language like Rust in a reasonable way.  Plus also you get a lot of
proof obligations about integer overflow, unless you use bignums.  On
the other hand, there's a C++11 back end for Purescript (purescript.org)
that uses std::shared_ptr as a poor person's GC, so maybe Rust has
something like that too.

Regarding verifying compilers, have you looked at the CompCert papers?
http://compcert.inria.fr

> What if the entire English-prose ARM were re-written as Coq proofs?

How about writing an Ada front end for CompCert?  I don't have any idea
about the commercial licensing terms though.  There's a company that
handles it but I've never looked into it.

Re: Why not Coq2Ada program extraction?

[Chris M Moore]

On 01/05/2018 04:59, Paul Rubin wrote:
> "Dan'l Miller" <optikos@verizon.net> writes:
>> Why hasn't anyone ever developed Ada extraction from Coq proofs?

I think we all have day jobs.

> That's interesting to hear about Rust.  Coq (like Ocaml, Scheme, and
> Haskell) is lambda calculus once you look past the types, so extracting
> to those languages is natural.  This gets back to our earlier
> discussion: lambda calculus is a computational model equivalent to a
> Turing machine, with unlimited memory.  You can translate the lambda
> calculus computational part to actual machine code, but you end up
> simulating the unlimited memory using garbage collection.  There's a
> book about it here:
> 
> https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/

You are not not necessarily forced to use garbage collection when 
implementing FP.  See section 19.3.2 Optimisation Using A Stack Model in 
the document you reference.

<snip>

Chris

-- 
sig pending (since 1995)

Re: Why not Coq2Ada program extraction?

[Paul Rubin]

Chris M Moore <zmower@ntlworld.com> writes:
> You are not not necessarily forced to use garbage collection when
> implementing FP.  See section 19.3.2 Optimisation Using A Stack Model
> in the document you reference.

Yes, compilers do those optimizations when they can.  It's not always so
simple.  Maybe you can figure out ways to do without it, but it makes
your work a lot harder, and the idea of programming is to shift work
from humans to computers.  So I never feel "forced" to use a GC.  I'm
happy to use one whenever I can.  There are times when I'm forced *not*
to use it, typically because of hardware or realtime constraints.  I'm
interested in Ada mostly to help deal with those situations.

Re: Why not Coq2Ada program extraction?

[Jeffrey R. Carter]

On 05/01/2018 05:38 AM, Dan'l Miller wrote:
> 
> Why hasn't anyone ever developed Ada extraction from Coq proofs?  Perhaps the coq2rust work-in-progress can serve as a guide and/or inspiration for an analogous coq2ada.

Sounds interesting. When do you expect to have it finished?

-- 
Jeff Carter
"My little plum, I am like Robin Hood. I take from
the rich, and I give to the poor. ... Us poor."
Poppy
96

Re: Why not Coq2Ada program extraction?

[Paul Rubin]

"Dan'l Miller" <optikos@verizon.net> writes:
> Why hasn't anyone ever developed Ada extraction from Coq proofs?
> Perhaps the coq2rust work-in-progress can serve as a guide and/or
> inspiration for an analogous coq2ada.

It also occurs to me that Ada wouldn't benefit as much from Coq proofs
as Rust does, since Ada already has SPARK, which is probably better
suited for Ada (and Rust)'s style of programming.  I know some people
also use Isabelle on Ada programs somehow.

Your idea of developing a formal semantics for Ada might be more
worthwhile than working on extraction from Coq.  A quick web search
found this:

https://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/19950018214.pdf

The page loads awfully slowly but it does finish after a while.

Re: Why not Coq2Ada program extraction?

[Jere]

On Tuesday, May 1, 2018 at 12:00:00 AM UTC-4, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > Why hasn't anyone ever developed Ada extraction from Coq proofs?
> On the other hand, there's a C++11 back end for Purescript (purescript.org)
> that uses std::shared_ptr as a poor person's GC, so maybe Rust has
> something like that too.
> 

You generally don't use any direct allocation or deallocation in Rust.  If
you need heap memory, you use something like Box<Element_Type> (like 
std::unique_ptr), Rc<Element_Type> (like std::shared_ptr), or 
Arc<Element_Type> (a thread safe version of Rc).  You generally don't use
pointers, but rely on references (which are always non-null and cannot be
deallocated).  Everything tries to be stack allocated if possible.  One of
the more confusing things that caught me was I kept seeing the use of 
SomeType::new() everywhere and assumed it was heap allocation.  It actually
rarely was heap allocation at all.  Also keep in mind that rust is actually
considered two different languages "safe rust" and "unsafe rust", which is
analogous to Ada's "unchecked" options.  You have to be explicit to use
unsafe rust and I believe there are language options to prohibit it's use
in your own code (I'd have to check to make sure on that though).  Pointers
are always "unsafe" so you cannot use them in Rust code without using
explicitly "unsafe Rust" code.  It is also very extremely picky about
how you use references.  You can only have either 1 mutable reference OR
up to N immutable references (never both).  It is all compile time checked
and the compiler is EXTREMELY picky (way more so than an Ada compiler is).

Re: Why not Coq2Ada program extraction?

[Dan'l Miller]

On Tuesday, May 1, 2018 at 3:21:39 AM UTC-5, Jeffrey R. Carter wrote:
> On 05/01/2018 05:38 AM, Dan'l Miller wrote:
> > 
> > Why hasn't anyone ever developed Ada extraction from Coq proofs?  Perhaps the coq2rust
> > work-in-progress can serve as a guide and/or inspiration for an analogous coq2ada.
> 
> Sounds interesting. When do you expect to have it finished?

The better question is when do I have enough •funding• of some sort to •start• in earnest?

Re: Why not Coq2Ada program extraction?

[G.B.]

On 01.05.18 05:59, Paul Rubin wrote:
> I wouldn't have thought it possible to extract to Coq a non-GC'd
> language like Rust in a reasonable way.  Plus also you get a lot of
> proof obligations about integer overflow, unless you use bignums.

I imagine that proofs of algorithms involving arbitrarily large
integers might be more tricky than expected as their representations
incur complexity WRT execution time and memory requirements. Unless,
of course, one is free to ignore space and time, which, AIUI is
not typical of (idealized) Ada programs.

OTOH, what typical Ada programs would ever need large integers?
Given that BigNums cannot well be used for indexing storage, e.g.,
will every data structure need to become a list of conss under
the hood?

One of the things that this dilettante likes about Haskell is
that it doen't ignore distinct types of number as essential.
I find it a good hint, though, that I shouldn't be using those
representational types in interfaces.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff

Re: Why not Coq2Ada program extraction?

[Paul Rubin]

"G.B." <bauhaus@notmyhomepage.invalid> writes:
> I imagine that proofs of algorithms involving arbitrarily large
> integers might be more tricky than expected as their representations
> incur complexity WRT execution time and memory requirements. Unless,
> of course, one is free to ignore space and time, which, AIUI is
> not typical of (idealized) Ada programs.

Right, this is why I'm taken slightly aback by the concept of extracting
Ada or Rust from Coq.  I wonder how stylized the Coq proofs have to be
for the extraction to work usefully.  Usually in extracted Coq proofs,
space and time are indeed ignored: the proof is only that the right
answer is eventually reached, space permitting.

Fwiw, Coq proofs extracted to (say) Haskell is crazy ugly, with unsafe
casts all over the place.  Coq can prove that the casts are safe, but
Haskell's type system isn't precise enough to understand the proofs, so
Coq has to tell it "trust me".  Extracted code in Rust or Ada might have
similar issues.

> One of the things that this dilettante likes about Haskell is
> that it doen't ignore distinct types of number as essential.

I'm not sure what you mean, but Haskell has separate Int (machine sized)
and Integer (arbitrary size) integers.  That they are separate types is
annoying and I think Haskell might have been better off handling the
issue some different way.

Re: Why not Coq2Ada program extraction?

[Dan'l Miller]

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.

Re: Why not Coq2Ada program extraction?

[Paul Rubin]

"Dan'l Miller" <optikos@verizon.net> writes:
> 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

The concept of "extraction" doesn't make as much sense with Isabelle
since it's not a programming language in the way Coq is.  You might like:

 http://concrete-semantics.org

Re: Why not Coq2Ada program extraction?

[Dan'l Miller]

On Sunday, May 6, 2018 at 9:37:27 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > 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
> 
> The concept of "extraction" doesn't make as much sense with Isabelle
> since it's not a programming language in the way Coq is.

But HOL4 and HOL-omega are.  They are standard ML.

>  You might like:
> 
>  http://concrete-semantics.org

Thank you.  I have downloaded the free PDF of that book at:
http://concrete-semantics.org/concrete-semantics.pdf

Re: Why not Coq2Ada program extraction?

[Dan'l Miller]

On Sunday, May 6, 2018 at 9:37:27 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > 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
> 
> The concept of "extraction" doesn't make as much sense with Isabelle
> since it's not a programming language in the way Coq is.

Here is an intro to the somewhat analogous codegen from HOL4:
https://isabelle.in.tum.de/doc/codegen.pdf

AIUI, Isabelle adopts HOL4 (instead of, say, FOL or ZF or Leslie Lamport et al's HOL-TLA or Leslie Lamport et al's HOL-TLA+ or Peter Vincent Homeier et al's HOL-omega) as its default system of logic, even though these five & others are installable instead.

Re: Why not Coq2Ada program extraction?

[Paul Rubin]

"Dan'l Miller" <optikos@verizon.net> writes:
> Here is an intro to the somewhat analogous codegen from HOL4:
> https://isabelle.in.tum.de/doc/codegen.pdf

Thanks, that is interesting.  I've heard of Isabelle/HOL being used for
verification in connection with Ada, but hadn't looked at it closely and
thought it worked somewhat differently.

Re: Why not Coq2Ada program extraction?

[Dan'l Miller]

On Sunday, May 6, 2018 at 9:30:14 PM UTC-5, Dan'l Miller wrote:
> 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

For those readers who are casually following along with these threads about theorem provers as potential correctness verifiers for Ada in the future:
Q:  What is that Hoare-triple stuff in the HOL4 machine-code verification?  A:  Here is an introduction:
http://www.cl.cam.ac.uk/%7Emom22/arm-hoare-logic.pdf

Re: Why not Coq2Ada program extraction?

[Dan'l Miller]

On Sunday, May 6, 2018 at 11:20:23 PM UTC-5, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > Here is an intro to the somewhat analogous codegen from HOL4:
> > https://isabelle.in.tum.de/doc/codegen.pdf
> 
> Thanks, that is interesting.  I've heard of Isabelle/HOL being used for
> verification in connection with Ada, but hadn't looked at it closely and
> thought it worked somewhat differently.

Isabelle is based on type inhabitation of various systems of logic into a generic kernel weak-type-theory system (an interface of sorts, if you will) in which various stronger systems of logic can be written (or plugged in, if you will).
https://en.wikipedia.org/wiki/Logical_framework

from https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)
“Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like first-order logic (FOL), higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification.”