Andrej Bauer <Andrej.Bauer <at> andrej.com> 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,
Chris