Re: [Caml-list] Unsoundness is essential

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-10-04 at 17:04 +0200, Andrej Bauer wrote:
[]

Thanks. I think this is a very good interpretation of my intent.

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

That's not quite right: it isn't that typing prevents me writing
my programs (it does sometimes, but usually that indicates
a design fault). It's more like the lack of expressiveness prevents
me writing down the invariants and so forth I actually want to.
I have to keep them in my head, or write them as comments where
they're not sanity checked.

In Felix for example the standard library contains this:

// additive symmetric group
typeclass FloatAddgrp[t] {
  inherit Eq[t];
  virtual fun zero: 1 -> t;
  virtual fun add: t * t -> t;
  virtual fun neg: t -> t;
  virtual fun sub(x:t,y:t):t => add (x,neg y);

  reduce id (x:t): x+zero() => x;
  reduce id (x:t): zero()+x => x;
  reduce inv(x:t): x-x => zero();
  reduce inv(x:t): - (-x) => x;
  axiom sym (x:t,y:t): x+y == y+x;
}

typeclass Addgrp[t] {
  inherit FloatAddgrp[t];
  axiom assoc (x:t,y:t,z:t): (x+y)+z == x+(y+z);
  reduce inv(x:t,y:t): x+y-y => x;
}

and here I can encode a LOT more information about the type T
the typeclass describes than Haskell allows. Furthermore,
the 'reduce' axioms have operational semantics (Felix really
does apply these reductions) and the axioms can be tested by
using a statement like 

	check(1,2);

which is how I discovered floating point arithmetic isn't
associative -- an actual regression test failed. What is more
Felix allows a 'lemma' which is an axiom which is made into
a proof goal in Why format for submission to a theorem prover.

This notation is weak, and the Felix compiler cannot really 
prove much with it: for example it does not check instances 
of typeclasses meet their obligations.

But at least the semantics are encoded in the language
and type checked, I can make reasoned arguments based on the
stated semantics, and there is some hope someone will come
along and implement some actual proof procedures and/or
optimisations at a later date.

[I really have proven one trivial lemma using both Ergo
and Simplify.]

Vincent Aravantinos made the important point:

"If you allow everything (such as the "type expressive" C you are  
envisaging), the programmer will be tempted to use this "everything"  
whereas he could achieve the same with a "bounded" language."

and the admission of semantics into the system is the starting
point for allowing one to at least state some of those bounds
(even if there is little or no enforcement the bounds are
formalised).

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

Ooops, I am sprung!

>  Skaller seems to 
> think that the only option is to give up safety, as well, with which I 
> disagree. We need _controlled_ unsafety.

Actually I HOPED someone smart enough would dare make such a proposal.
I think I alluded to this idea in the claims that adding unsound
typing to the existing Ocaml type system such as non-zero integers
will not actually compromise safety, but rather enhance it.

However I just do not understand how to say 'It is safe up
to this point, and risky from there on'. I have no mental
concept of 'delimited unsoundness'.

In an analogous context I had no idea how to mix side-effecting
and functional code in a delimited way until I saw how Haskell
does it with Monads.

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

Of course, all pragmatic compilers offer switches to control this
kind of thing.

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

Ah.

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

This is quite good from an industrial viewpoint. The list of
assertions can be reduced by more work in selective areas
as a complement to testing. This gives managers control over risk.

It seems a consequence of this manifesto is that the asserting
of the assertions, if not their proofs, need to be encoded
into the program in an effort to reduce the size of the output
list.

A difficulty here is saying the assertions in a comprehensible
way which is well coupled to the original code. As you said
previously, this probably requires an interactive system.


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net