skaller a écrit : > On Wed, 2007-10-03 at 19:28 -0400, Joshua D. Guttman wrote: >> skaller writes: >> >>> Goedel's theorem says that any type system strong enough >>> to describe integer programming is necessarily unsound. > > I paraphrased it, deliberately, in effect claiming an analogous > situation holds with type systems. > Not unsound, incomplete ! you mixup first and second incompleteness theorem. Let's clarify ? - first if a type system does not contain arithmetic nothing can be said (this implies ML), but in this case, the meaning of complete needs to be clarified. Indeed, there are complete type system ... - The 1st incompleteness theorem states that no theory containing arithmetic is complete. This means that there will always be correct programs that your type system can not accept. However, I thing a real program that is not provably correct in lets say ZF, does not exists and should be rejected. you do not accept a program whose correctness is a conjecture (do you ?) - The second incompleteness theorem, states that a system that proves its own consistency is in fact inconsistent. For type system (strong enough to express arithmetic, like ML with dependant type, PVS, the future PML, ..). This means that the proof that the system is consistent (the proof that "0 = 1 can not be proved") can not be done inside the system. However, the proof that your implementation does implement the formal system correctly can be done inside the system, and this is quite enough for me. - The soundness theorem for ML can be stated as a program of type "int" will - diverge - raise an exception - or produce an int I think everybody except LISP programmers ;-) want a sound type system like this. OK replace everybody by I if you prefer ... For PML, we are more precise : exception and the fact the a program may diverge must be written in the type. - ML type system is sometimes too incomplete, this is why the Obj library is here. However, the use of Obj is mainly here because ML lacks dependant types. In fact, the main use of Obj is to simulate a map table associating to a key k a type t(k) and a value v:t(k). - All this says that a type-system only accepting proved programs is possible and a good idea (it already exists). The question for researcher is how to produce a type system where the cost of proving is acceptable compared to the cost of debugging, and this stars to be the case for some specific application, but we are far from having to remove the word "bug" from our vocabulary ;-) -- Christophe Raffalli Universite de Savoie Batiment Le Chablais, bureau 21 73376 Le Bourget-du-Lac Cedex tel: (33) 4 79 75 81 03 fax: (33) 4 79 75 87 42 mail: Christophe.Raffalli@univ-savoie.fr www: http://www.lama.univ-savoie.fr/~RAFFALLI --------------------------------------------- IMPORTANT: this mail is signed using PGP/MIME At least Enigmail/Mozilla, mutt or evolution can check this signature. The public key is stored on www.keyserver.net ---------------------------------------------