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: Tue, 01 May 2018 02:12:52 -0700
Organization: A noiseless patient Spider
Message-ID: <87tvrrlox7.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="385ce2792b816f56a692583465018913";
	logging-data="6655"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19srfv2hzCRNGm9ShXVvsCQ"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:ecN2SNmzTXzd+eE+/Jv3oBD0P7w=
	sha1:bMX/myU5BcVPTcK1ezKZpikiIBs=
Xref: reader02.eternal-september.org comp.lang.ada:51876
Date: 2018-05-01T02:12:52-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?
> 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.