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 00:41:37 -0700
Organization: A noiseless patient Spider
Message-ID: <8736zbn7pq.fsf@nightsong.com>
References: <7b6ae5e8-6604-4d36-b606-ead71f667847@googlegroups.com>
	<87efiwm3er.fsf@nightsong.com> <ufUFC.74642$eg.39849@fx43.am4>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="385ce2792b816f56a692583465018913";
	logging-data="11475"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19W5RS19ZrYlF1MyhumwlOw"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:/hurLmbAGWgXnQ7Bzcur05RK1jw=
	sha1:fsvLMIKNRNiwPv7E7qqUujF+IWY=
Xref: reader02.eternal-september.org comp.lang.ada:51872
Date: 2018-05-01T00:41:37-07:00
List-Id: <comp.lang.ada>

Chris M Moore <zmower@ntlworld.com> writes:
> You are not not necessarily forced to use garbage collection when
> implementing FP.  See section 19.3.2 Optimisation Using A Stack Model
> in the document you reference.

Yes, compilers do those optimizations when they can.  It's not always so
simple.  Maybe you can figure out ways to do without it, but it makes
your work a lot harder, and the idea of programming is to shift work
from humans to computers.  So I never feel "forced" to use a GC.  I'm
happy to use one whenever I can.  There are times when I'm forced *not*
to use it, typically because of hardware or realtime constraints.  I'm
interested in Ada mostly to help deal with those situations.