Re: Why not Coq2Ada program extraction?

["G.B." <bauhaus@notmyhomepage.invalid>]

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