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 _______________________________________________ Caml-list mailing list. Subscription management: http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list Archives: http://caml.inria.fr Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
