Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[OSR] Standard syntax extensions ?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2008-04-27 (14:20)
From: Christopher L Conway <cconway@c...>
Subject: Re: [OSR] Standard syntax extensions ?
Andrej Bauer <Andrej.Bauer <at>> writes:
> Arthur Chan wrote:
> > That
> > said, there are some of us who feel that that the python infix syntax is
> > clearer, and as it corresponds more directly to the mathematical
> > notation, it is just as provably correct as the List.mem notation is. 
> > If reusing "in" is a big deal, then maybe we could do "in_list" or
> > "inlist"?  That'd be more type-safe too.
> Just a small correction, if you will alow me. When we speak of
> correctness of a programming language we do not say that "syntax is
> provably correct" but rather that the "implementation is correct".

I think what Arthur meant by "provably correct" was "has well-defined semantics,
aiding proofs of correctness."

> Actually, the whole phrase "provably correct" is often misused in
> computer science, at least the way I understand it. If you prove
> something then it is "proved correct", while a thing is "provably
> correct" if we _could_ prove it correct. Perhaps a native speaker of
> English can clarify this point.

You have a point, from a prescriptive point of view. But in the common usage
"provable" and "proved" are sometimes interchanged. Most computer scientists
aren't Platonists: "provable" means "I could describe the proof for you, step by
step, if you like, but let's save some time by skipping it." Saying a claim is
"provable" without working out the proof begs the question.

> Isn't everything on this list a minor quibble? 

Happy quibbling,