Re: Why not Coq2Ada program extraction?

[Jere <jhb.chat@gmail.com>]

On Tuesday, May 1, 2018 at 12:00:00 AM UTC-4, Paul Rubin wrote:
> "Dan'l Miller" writes:
> > Why hasn't anyone ever developed Ada extraction from Coq proofs?
> On the other hand, there's a C++11 back end for Purescript (purescript.org)
> that uses std::shared_ptr as a poor person's GC, so maybe Rust has
> something like that too.
> 

You generally don't use any direct allocation or deallocation in Rust.  If
you need heap memory, you use something like Box<Element_Type> (like 
std::unique_ptr), Rc<Element_Type> (like std::shared_ptr), or 
Arc<Element_Type> (a thread safe version of Rc).  You generally don't use
pointers, but rely on references (which are always non-null and cannot be
deallocated).  Everything tries to be stack allocated if possible.  One of
the more confusing things that caught me was I kept seeing the use of 
SomeType::new() everywhere and assumed it was heap allocation.  It actually
rarely was heap allocation at all.  Also keep in mind that rust is actually
considered two different languages "safe rust" and "unsafe rust", which is
analogous to Ada's "unchecked" options.  You have to be explicit to use
unsafe rust and I believe there are language options to prohibit it's use
in your own code (I'd have to check to make sure on that though).  Pointers
are always "unsafe" so you cannot use them in Rust code without using
explicitly "unsafe Rust" code.  It is also very extremely picky about
how you use references.  You can only have either 1 mutable reference OR
up to N immutable references (never both).  It is all compile time checked
and the compiler is EXTREMELY picky (way more so than an Ada compiler is).