The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Randy Pollack wrote:
> BTW, I guess coercions are required for large scale formal
> mathematics.  For example, subtyping of algebraic structures by purely
> structural means (fewer components, ...) is inadequate for real
> mathematics.
>    

I'm willing to believe that's true.  I would still expect that program 
verification can get on pretty well with no coercions, type classes, 
setoids, or other sources of fanciness. ;)