Re: [Caml-list] Unsoundness is essential

[Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>]

I too have a compulsive obsession to talk about logic, so here is my 
contribution.

Logic is about details. It is only to be expected that in a willy-waving 
competition on a mailing list like ours everyone will get something 
wrong about such a tricky thing as Goedel's theorems (me included). For 
example:

Christophe Raffalli:
> - 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 ...

In logic complete usually means: for every sentence A the system proves 
A or it proves not A. This has nothing to do with being able to 
interpret arithmetic. We can define completeness without reference to 
arithmetic.

(Presumably, a type system is complete if for every (closed) type A,
A is inhabited or A -> void is inhabited. At least this would be the 
reading of completeness under propositions-as-types.)

Christophe Raffalli:
> - The 1st incompleteness theorem states that no theory containing
> arithmetic is complete.

No _sound_ theory interpreting arithmetic is complete.

Arnaud Spiwack wrote:
> 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).

Goedel's theorems say nothing directly about truth. This is a common 
misconception.

Skaller started the discussion with a rerefence to Geodel, which he did 
not attempt to use in a technically correct way. I think it would be 
beneficial for this discussion to move away from explicit references to 
Goedel.

We seem to be talking about two things:

a) Expressiveness of a type system vs. decidability of type-checking.

The main point is that the more expressive the type system the harder it 
is to check types.

b) Safety guarantees for well-typed programs

A typical safety guarantee is expressed with the Preservation Lemma 
("Types are preserved during evaluation") and Progress Lemma ("A typed 
program is either a value or has a next evaluation step"). Together 
these two imply, e.g., that there won't be a segmentation fault.

I think to some extent (b) is what skaller calls "soundness".

If I read skaller correctly, he made three points (please correct me if 
not):

1) The safety properties of well-typed programs in C are none,
but Ocaml is not much better either, since it just pretends that 
exceptions are safe. Therefore, to at least some degree the slogan "the 
Ocaml type system guarantees safety" is not entirely and honestly true.

2) Morally inferior languages such as C and Python are popular because 
people are not willing to write programs with their hands tied to their 
backs by a typing system.

3) Skaller would rather have poor safety guarantees than an inexpressive 
type system that ties his hands.

Goedel is dragged in only because his theorems tell us that the perfect 
world does not exist, i.e., we cannot have decidable type checking of a 
very expressive type system which also has sane safety properties.

Leaving Goedel aside for a moment, we can ask what a good practical 
combination of expressiveness and safety would be. We have to give up at 
least one of the three desired properties (expressiveness, decidability 
of type checking, safety). Various languages make various choices, as 
was already mentioned in this thread. Let me just say that the choice 
made by C, i.e., to give up both expressiveness and safety in return for 
easy type-checking is not as crazy as it may sound (imagine it's 1970, 
your computer has 4kb of memory, everybody around you thinks of types as 
hints to compilers about how many bytes of storage a variable will take, 
and Martin-Lof is just an obscure Scandinavian mathematician and/or 
philosopher that real programmers never heard of).

It seems to me that the evolution of theory-backed languages such as ML 
and Haskell is reaching a point where people are willing to give up 
decidability of type-checking (Haskell has done it). Skaller seems to 
think that the only option is to give up safety, as well, with which I 
disagree. We need _controlled_ unsafety.

My position is this:

i) Insist on good safety properties. If a program compiles without any 
"ifs" and "buts", then it is safe (whatever that means). It the compiler 
thinks the program might be unsafe it should try to compile anyhow, and 
tell us why precisely it thinks it might be unsafe.

ii) Give programmers very expressive type systems so that they can write 
things like

    div : int * {x : int | not (x = 0)} -> int

and much more.

iii) Of course, by combining i) and ii) we must then give up 
decidability of type-checking. We can compensate for that loss by 
_making compilers more interactive_. The current model, where a compiler 
either succeeds on its own or fails completely, is not going to take us 
much further. People from the automated theorem proving community learnt 
a while ago that the interaction between the human and the computer is 
the way to go.

A compiler should be able to take hints on how to check types. The 
result of compilation should be one of:

- everything is ok

- the program contains a grave typing error which prevents
   the compiler from emitting sane code, compilation is aborted

- the compiler generates sane code but also emits a list of assertions
   which need to be checked (by humans or otherwise) in order to
   guarantee safety

If we had compilers like that, they would greatly encourage good 
programming practices.

You can read the above as my manifesto, if you wish.

Best regards,

Andrej