Re: [Caml-list] Unsoundness is essential

[Christophe Raffalli <christophe.raffalli@univ-savoie.fr>]

[-- Attachment #1: Type: text/plain, Size: 3140 bytes --]

skaller a écrit :
> On Wed, 2007-10-03 at 19:28 -0400, Joshua D. Guttman wrote:
>> skaller <skaller@users.sourceforge.net> 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
---------------------------------------------


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 252 bytes --]