From: skaller <skaller@users.sourceforge.net>
> On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:
> 
> > Yet, modules are strange beasts for typing, so I wouldn't add the code
> > before thinking it through.
> 
> I am curious as to the status of COQ support for verifying
> assertions about proposed changes to the type system.
> 
> For example supposing you did 'think it through' and it
> seemed right, would you be able to then extend an
> existing COQ proof and attempt to prove your thinking
> mechanically?

Unfortunately, I'm afraid we are still pretty far from that.
Supposing we could describe all the properties we need in Coq
(probably possible, but far from easy), a very long and harduous
proof is waiting.
If there is a breakthrough, I would be most happy to check everything,
as I know there are bugs in the compiler. I just discovered a stupid
unsoundness today.

Jacques Garrigue