The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Le 20/01/2021 à 20:45, Adam Chlipala a écrit :

> Also, if you really want good performance, why not verify a program in 
> some deeply embedded language?  I've found performance predictability to 
> be quite treacherous within normalization of Gallina terms.  I'd much 
> rather generate a C program with a proof that it computes the answer I 
> want.  Many potential target languages allow your proposed optimization 
> to be /proved/ from first principles.

Alternatively, why not generate an OCaml program (using Coq extraction) 
that computes the answer ? This seems a much simpler approach.

Actually, this is exactly the approach taken in the paper given in my 
previous answer...

Sylvain.