Re: [Caml-list] Equality of functional values

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

On Wed, 2007-01-31 at 00:06 +0100, Andrej Bauer wrote:
> skaller wrote:
> > Actually the idea 'equality of functions is not computable'
> > is misleading .. IMHO. Equality of programmer written
> > 'functions' should always be computable: more precisely one hopes
> > every function could have a mechanically verifiable proof
> > of correctness and wished programming languages provided an 
> > easy way to prove one.
> 
> There are two major reasons why equality of functions might not be 
> computable in a specific situation:
> 
> 1) Sufficiently general functions are allowed so that various 
> diagonalization theorems kick in and we get a proof that equality is not 
> decidable.

You're right. Canonical example for me: my own Felix compiler :)
[Encodes functions as data .. Felix language is Turing complete .. :]

> 2) The functions are "simple", but they are represented in such a way 
> that they cannot be tested for equality.
> 
> The first reason is more "theoretical" (but still underappreciated by 
> "real" programmers),

:) I love this list because there are theoreticians who are
ready to educate us 'real' programmers. 

> To summarize what I wrote above: it may be a matter of how functions are 
> represented, not _which_ functions we are trying to compare.

You're right: that was a very nice explanation!

> > BTW: Felix is one of the few general languages around that
> > actually allows a statement of semantics:
> > 
> > typeclass SemiGroup[t with Eq[t]] {
> >   virtual fun add: t * t -> t;
> >   axiom assoc(x:t, y:t, z:t): add(x, add(y,z)) == add(add(x,y),z);
> > }
> > 
> > These axioms are checkable:
> > 
> > instance SemiGroup[int] {
> >   fun add:int * int -> int = "$1+$2";
> > }
> > 
> > axiom_check(1,2,3);
> 
> You are confusing checking of particular instances and checking the 
> general statement in which x, y and z, are universally quantified.

The 'axiom_check' facility clearly only checks particular
instances and would only provide a proof if you could
exhaustively elaborate all such instances.

> Checking of particular instances may still be valuable to a programmer, 
> though, as it is a form of run-time correctness checking.

Yes. My experience is that it catches quite a lot of errors.
Proof would be better .. but I don't know how to do that.

> > however there's currently no way to state and prove
> > theorems. It would be interesting if someone had some
> > idea how to use one of the existing theorem provers
> > to act as a proof assistant (verify user given proof,
> > filling in enough 'gaps' in the formal steps to make
> > it practical).
> 
> I would go further: it would be interesting to augment real programming 
> languages with ways of writing specifications that can then be tackled 
> by theorem provers and proof asistants. 

I don't think you're going further .. I'm actually asking that
question! I have looked at Coq, HOPL (light) etc, in the hope
there is some way of using them to complete programmer proof
sketches, but all still seem to need very heavy assistance
beyond the understanding of a non-expert.

> In the long run this might 
> educate programmers about the value of correct programs. Naturally, as 
> long as only Mars space probes and the occasional airplane crash because 
> of software errors, there won't be sufficient economic incentive to 
> wrote correct software.

I believe that this isn't so: there is plenty of incentive
to write correct software. Industry does monitor maintenance
cost of software compared to cost of creating it. We don't need
a plane crash to demonstrate the need for correctness,
in fact that wouldn't help much because the costs aren't
so easy to measure. Wages of people working on maintenance
are measured regularly by all large organisations.

Yet people still use PHP, Python, Java .. why?
Industry may be stupid but it isn't *entirely* stupid :)


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