Re: [Caml-list] Unsoundness is essential

[Arnaud Spiwack <aspiwack@lix.polytechnique.fr>]

Hi everybody,

Christophe already said much of what I have to do, but it's compulsively 
impossible to me to avoid posting on such a thread. My own 
psychopathologies coerce me into meddling into here.

First of all, as some sort of an introductory thing, I'd like to mention 
that Java is probably the currently most popular language among 
programmers, and it's strongly typed. Indeed, there are quite a few 
unsafe feature (null pointers,
down casting), but they are gradually removed (well, I guess null 
pointers won't ever): since the addition of generics
wild downcasting to use generic structures is largely deprecated, if one 
would provide with a primitive ternary guarded
cast operator, one wouldn't have to resort to write it by hand "if 
(blah.isClass...", etc...

Anyway, back to Mr. Gödel and his theorem. What he stated indeed is that 
truth and provability never coincide (provided we're talking of 
something at least as expressive as arithmetic). That is, as some people 
already mentionned:
either everything can be proved, or there is at least a statement A such 
that neither A is provable neither its negation.

Still there is something peculiar in the interpretation of Gödel 
theorem, since if we are in a classical logical system (where ~~A (not 
not A)  and A are equivalent). If neither A nor ~A are provable, then 
both can be "the real one". By that I mean that both can be chosen as 
true, without impacting the consistency of the system (quick proof 
sketch : A -> ~A is equivalent to A -> (A -> False) which is equivalent 
to A&A -> False wich is equivalent to ~A).

A conclusion I can draw from that is that we don't care about what is 
true, we care about what is provable, since it is at least welle 
defined, where truth is very much unclear (an example of such weirdness 
is the axiom of choice, which is a very pratical axiom in classical 
mathematics, and widely accepted. Except when you are doing 
probabilities where it
is very convenient to have the "measurability axiom" stating that 
"everything is mesurable" (more or less) and which contradicts the axiom 
of choice).

Now let's move to programming again. Type systems can be arbitrarily 
complex, see for instance, Coq, Agda2, Epigram, PML and many other that 
I'm less familiar with. In this language, evidences show that everything 
one needs
to prove for proving a program (partially) correct, is provable. There 
we must draw a clear line between two concept
which have been a bit mixed up in this thread : provability and 
decidability. Of course, it is not possible to decide in all
generality that whoever integer is non-zero, thus a type system able to 
express (int -> int-{0} -> int) as a type for division cannot decide 
type checking without extra information. The extra information is no 
more than a proof that we never provide an 0-valued integer (at each 
application). And curry-howard isomorphism allows to stick it inside the 
type system. That's what Type Theorist yearn for (by the way that is 
cool because many runtime check consume
time unneedlessly, and time is money, and money is precious).

Of course, there is still a lot of work to do around these. But this is 
more than promissing, and one should be able to never need unsafe 
features (though there actually is a more or less unsafe feature 
inherently in these type systems, it's called "axioms", since you can 
generaly enhance the theory with any additional claim. However axioms 
are usually kept out of very sensitive areas).

At any rate, this does not say anything about the mostly untype 
languages. It is a different issue, typed vs untyped or decidable type 
inference vs more expressiveness in type system. The untyped world has 
its perks, especially C, which allow quite a few low level manipulation 
which are very useful. What I mean here is that if we need types (and I 
believe that a vast majority of programming application do), then we 
should have as expressive typing as possible, and not need to rely on 
unsafe feature which give headaches and segfaults.


I realize that I got lost in my way, so I'll stop here, but I may be 
back (this is a much more prudent claim than that of another AS) in 
followups ;) .


Arnaud Spiwack

Christophe Raffalli a écrit :
> 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 ;-)
>
>   
> ------------------------------------------------------------------------
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>