From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: Why not Coq2Ada program extraction?
Date: Tue, 01 May 2018 02:12:52 -0700
Date: 2018-05-01T02:12:52-07:00 [thread overview]
Message-ID: <87tvrrlox7.fsf@nightsong.com> (raw)
In-Reply-To: 7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.com
"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.
next prev parent reply other threads:[~2018-05-01 9:12 UTC|newest]
Thread overview: 17+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-05-01 3:38 Why not Coq2Ada program extraction? Dan'l Miller
2018-05-01 3:59 ` Paul Rubin
2018-05-01 6:59 ` Chris M Moore
2018-05-01 7:41 ` Paul Rubin
2018-05-01 11:44 ` Jere
2018-05-02 16:47 ` G.B.
2018-05-02 17:12 ` Paul Rubin
2018-05-01 8:21 ` Jeffrey R. Carter
2018-05-01 17:30 ` Dan'l Miller
2018-05-01 9:12 ` Paul Rubin [this message]
2018-05-07 2:30 ` Dan'l Miller
2018-05-07 2:37 ` Paul Rubin
2018-05-07 3:50 ` Dan'l Miller
2018-05-07 4:01 ` Dan'l Miller
2018-05-07 4:20 ` Paul Rubin
2018-05-07 16:33 ` Dan'l Miller
2018-05-07 13:27 ` Dan'l Miller
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox