The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/13/2016 01:00 PM, Maxime Dénès wrote:
> Hi Jonathan,
>
> On 09/13/16 17:51, Jonathan Leivent wrote:
> > it can interfere with the preservation of properties like complexity
> > between extracted code and the original Coq source.
> Can you elaborate a bit? I vaguely remember this being discussed on the
> list at some point, but I forgot what it was about.
>
> Thanks!
>
> Maxime.

Yeah - it was a briefly heated discussion a while ago.  I don't recall 
it that well, and I think I was one of the instigators.  My point here 
is not to re-raise it.  But, vaguely, the discussion had to do with 
various proxies for complexity that are not preserved by functional 
extensionality, yet otherwise might be of interest when doing Coq -> 
extracted code.  If instead one is limited to functional extensionality 
only on Prop functions, then the point (whatever it was) is obviously 
moot, as such functions don't contribute to extracted code at all.

-- Jonathan