The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thu, Nov 3, 2011 at 2:10 PM, Andrej Bauer <andrej.bauer AT andrej.com> wrote:

> So yes, it's probably useless if you need things to be
> computable at the end.  But if what you're doing is pure mathematical
> formalization, I don't see any drawbacks to using this construction.

Or you can be computable _and_ do pure mathematical formalization, to
get the best of both worlds.

I've tried that in the past, and usually found the overhead of keeping track of various setoids, inserting properness conditions for functions, etc. to be more than it was worth.  Especially if I was working with things like traditional topology or the Hilbert basis theorem which are non-constructive anyway.  (Yes, I know Groebner bases are an effective way to compute with ideals in polynomial rings, but I'm not sure how I'd state the Hilbert basis theorem in such a way that I could prove it constructively.  And even if a constructive statement is well known, like maybe "for any stream of elements of the ring, some element is in the ideal generated by the previous elements," that's sort of beside the point if what you what to prove is the traditional statement.)
--
Daniel Schepler