On 21-Feb-1999, Lennart Augustsson <[EMAIL PROTECTED]> wrote:
>
> [Fergus wrote:]
> > Well, yes, up to a point, but it may be clearer if the simple
> > regular types part is kept separate from the undecidable part,
> > as was done in NU-Prolog, or as is done in Eiffel.
>
> I'm not necesssarily advocating that the properties and proofs of these
> properties should be mixed with the regular code. That's just
> one way of doing it. Take sort as an example, we can do this
> (ignoring the compare function):
>
> sort :: (xs :: [a]) -> ListTypeWithProofOfCorrectnes xs
> sort xs = ... sort code with integrate proof
>
> or this
>
> sort :: [a] -> [a]
> sort xs = ... normal sort code
>
> sortReallySorts :: IsASortingFunction sort
> sortReallySorts = ... proof that sort really sorts
>
> Both of these styles are perfectly feasible to express in Cayenne.
> Which one to use depends on the situation (and your taste :-).
> I guess you prefer the latter.
I consider even the second one to be mixing the proofs
with the code, because there's no easy way that I can tell at
a glance that `sortReallySorts' is a proof rather than a program.
> BTW, has Eiffel changed? Last time I looked you could only
> have assertions checked at runtime, and no correctness proofs.
No, Eiffel hasn't changed.
> If you were talking about assertions, you might as well have said C. :-)
No, because in Eiffel the assertions are part of the interface
(part of the "type", if you wish, although syntactically separate
from the parts which are checked at compile time),
whereas in C they aren't.
> [Fergus wrote:]
> > [Lennart wrote:]
> > > I don't see how these properties can be expressed in a different way
> > > even if they were outside the types. You may object to the notation
> > > used, but give me a font with quantifiers and I'll make it look pretty. :-)
> >
> > You may be right, but I won't believe it until I see it ;-)
>
> Well, I won't believe that you can make it any easier by moving
> the proof out of the instance declarations. Defining what an
> equivalence relation is will look similar in other notations.
Other notations could make it much clearer which part is the program,
and which part is the proof.
--
Fergus Henderson <[EMAIL PROTECTED]> | "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh> | but source code lives forever"
PGP: finger [EMAIL PROTECTED] | -- leaked Microsoft memo.
