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: Wed, 02 May 2018 10:12:02 -0700
Organization: A noiseless patient Spider
Message-ID: <87h8nq3rtp.fsf@nightsong.com>
References: <7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.com>
	<87efiwm3er.fsf@nightsong.com> <pccq3q$gdj$1@dont-email.me>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="c542ccd1be7cc45dffb8a8de81e34fd0";
	logging-data="27411"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19mslKjwuLHg7b3UMatIte0"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:1ViP73bpi94O1yL7155dReFeAXU=
	sha1:8Mc8lelR3TOi5byle/vHqenxkfY=
Xref: reader02.eternal-september.org comp.lang.ada:51924
Date: 2018-05-02T10:12:02-07:00
List-Id: <comp.lang.ada>

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