winscape 2263

snip

Sure it is -- in a few places, anyway. It's taught mostly in theory clbuttes (*), at a few schools, and in general it's not well regarded by either the students or, as far as I know, the professional development community. (I would be pleased to be corrected on the latter point, but it's my impression.)

((*) These are the courses that strongly resemble math courses, and in which students are more likely to be asked to write proofs and solve math-like problems than to write programs. I say this only because sometimes when I say "theory" I seem to lead you astray .... )

A problem is that it may be difficult to teach this stuff in a way that connects with the real world -- or at least, that has been my experience in trying to teach the very basics of it in a math-for-CS-majors course. The notion of formally proving correctness is often introduced with trivial examples, where the cumbersome mechanisms of doing a line-by-line proof don't seem to add any value. "It's obvious this code works; why prove it?"

The textbook I often use includes a proof that Euclid's algorithm for finding greatest common divisor works. I think this is a much better example of the value of formal techniques. The algorithm is far from obvious, and coming up with a set of test cases .... Not so obvious either. But there is a nice proof, which whether it helps with understanding the algorithm or not, does make a good case for its correctness. To me this example demonstrates the value of the formal approach. I don't know how well it convinces the students.

I also try to convince the students that the same techniques, applied with slightly less detail and rigor, are really a help in thinking about whether programs work. The idea of a loop invariant, for example, is behind how I think about writing loops, and I'm fairly sure that my ability to write correct code improved dramatically when I was taught this approach in a course in graduate school. (It was an upper-division undergrad course in algorithms, taught by someone who believed in this kind of approach.)

A problem is that I teach this in the context of a course that's supposed to cover many other topics, and .... well, if there's a way to do it well in the time I have, I haven't found it. I think many instructors would just not bother, and yet this stuff is not, as far as I can tell, covered anywhere else in the curriculum, and I think it's shameful that students can graduate and not know what a loop invariant (in the context of formal proofs of correctness) is! Well, I guess we have finite time, and everyone thinks that their favorite topics are crucial ....

Doesn't it though. I'll leave it too.

-- B. L. Mbuttingill ObDisclaimer: I don't speak for my employers; they return the favor.