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:a0c:ab14:: with SMTP id
 h20-v6mr9792804qvb.60.1525195846773;
        Tue, 01 May 2018 10:30:46 -0700 (PDT)
X-Received: by 2002:a1f:b40b:: with SMTP id
 d11-v6mr2501639vkf.1.1525195846570;
 Tue, 01 May 2018 10:30:46 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!news.swapon.de!feeder.usenetexpress.com!feeder-in1.iad1.usenetexpress.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!x25-v6no9225323qto.0!news-out.google.com!c8-v6ni729qtc.0!nntp.google.com!x25-v6no9225320qto.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Tue, 1 May 2018 10:30:46 -0700 (PDT)
In-Reply-To: <pc982i$p9v$2@dont-email.me>
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>
 <pc982i$p9v$2@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <f10e977b-8a43-42fc-930e-a995b1f7e06b@googlegroups.com>
Subject: Re: Why not Coq2Ada program extraction?
From: "Dan'l Miller" <optikos@verizon.net>
Injection-Date: Tue, 01 May 2018 17:30:46 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 1693
X-Received-Body-CRC: 3318676403
Xref: reader02.eternal-september.org comp.lang.ada:51890
Date: 2018-05-01T10:30:46-07:00
List-Id: <comp.lang.ada>

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:
> >=20
> > Why hasn't anyone ever developed Ada extraction from Coq proofs?  Perha=
ps the coq2rust
> > work-in-progress can serve as a guide and/or inspiration for an analogo=
us coq2ada.
>=20
> Sounds interesting. When do you expect to have it finished?

The better question is when do I have enough =E2=80=A2funding=E2=80=A2 of s=
ome sort to =E2=80=A2start=E2=80=A2 in earnest?