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
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Why not Coq2Ada program extraction?
Date: Mon, 30 Apr 2018 20:59:56 -0700
Organization: A noiseless patient Spider
Message-ID: <87efiwm3er.fsf@nightsong.com>
References: <7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="d740b49da12eaabd4c203ceddc63754d";
	logging-data="14270"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/LIjTW8Ix1kvpGDIaR8m8i"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:dekN98Icc2RMYTDz3rzLnEaIEpg=
	sha1:l0GJBFemJALIj7xKLTFJKOABAgA=
Xref: reader02.eternal-september.org comp.lang.ada:51865
Date: 2018-04-30T20:59:56-07:00
List-Id: <comp.lang.ada>

"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.