Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Type constraints
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2004-12-09 (04:53)
From: Jacques Garrigue <garrigue@m...>
Subject: Re: [Caml-list] Type constraints
From: skaller <>
> 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