English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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 <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