Re: Why not Coq2Ada program extraction?

[Chris M Moore <zmower@ntlworld.com>]

On 01/05/2018 04:59, Paul Rubin wrote:
> "Dan'l Miller" <optikos@verizon.net> writes:
>> Why hasn't anyone ever developed Ada extraction from Coq proofs?

I think we all have day jobs.

> That's interesting to hear about Rust.  Coq (like Ocaml, Scheme, and
> Haskell) is lambda calculus once you look past the types, so extracting
> to those languages is natural.  This gets back to our earlier
> discussion: lambda calculus is a computational model equivalent to a
> Turing machine, with unlimited memory.  You can translate the lambda
> calculus computational part to actual machine code, but you end up
> simulating the unlimited memory using garbage collection.  There's a
> book about it here:
> 
> https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/

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.

<snip>

Chris

-- 
sig pending (since 1995)