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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@notmyhomepage.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Why not Coq2Ada program extraction?
Date: Wed, 2 May 2018 18:47:53 +0200
Organization: A noiseless patient Spider
Message-ID: <pccq3q$gdj$1@dont-email.me>
References: <7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.com>
 <87efiwm3er.fsf@nightsong.com>
Reply-To: nonlegitur@notmyhomepage.de
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 2 May 2018 16:47:54 -0000 (UTC)
Injection-Info: reader02.eternal-september.org;
 posting-host="2209a541ab018e20848fae8af258fc9a";
	logging-data="16819"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/dKm+U54n9vIt2WVniiaamdpQhal6jA8o="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:52.0)
 Gecko/20100101 Thunderbird/52.7.0
In-Reply-To: <87efiwm3er.fsf@nightsong.com>
Content-Language: de-DE
Cancel-Lock: sha1:FBaTcF+BJpQ8R7iGVZHnk9JSZbM=
Xref: reader02.eternal-september.org comp.lang.ada:51920
Date: 2018-05-02T18:47:53+02:00
List-Id: <comp.lang.ada>

On 01.05.18 05:59, Paul Rubin wrote:
> 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.

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.

OTOH, what typical Ada programs would ever need large integers?
Given that BigNums cannot well be used for indexing storage, e.g.,
will every data structure need to become a list of conss under
the hood?

One of the things that this dilettante likes about Haskell is
that it doen't ignore distinct types of number as essential.
I find it a good hint, though, that I shouldn't be using those
representational types in interfaces.

-- 
"HOTDOGS ARE NOT BOOKMARKS"
Springfield Elementary teaching staff