From: Paul Rubin <no.email@nospam.invalid>
Subject: Re: Why not Coq2Ada program extraction?
Date: Tue, 01 May 2018 00:41:37 -0700
Date: 2018-05-01T00:41:37-07:00 [thread overview]
Message-ID: <8736zbn7pq.fsf@nightsong.com> (raw)
In-Reply-To: ufUFC.74642$eg.39849@fx43.am4
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.
next prev parent reply other threads:[~2018-05-01 7:41 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 [this message]
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
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