Had this done to me, in 1981 or so at the University of MD. They decided to teach some kind of "theory of proving programs correct" to a bunch of CS-101 types who were just learning Pascal, too. I guess the hope was that we'd get a healthy dose of mathematical proofiness and write better programs.
One of our first lectures: "Taking this loop, we prove by induction that it computes the sum of the first ten integers. Here are a bunch of logic formulas (lots of scribbles on the overhead). Here's a bunch of notation, it's got CONJUNCTION and DISJUNCTION and COMPOSITION and so forth. By inference [and some hand-waving] this five line program computes a sum, yes?"
Class: "Huh?" Not even panic, just a collective, bug-eyed "<I>What the fuck?</I>?"
The approach failed miserably; what it /did/ successfully teach was cynicism; most of the students were really upset at the obvious nonsense. [I was the only one of about 250 students to complete all the project work . . . and I cheated by writing the project in LISP, and writing a LISP interpreter in Pascal]
Comments
Had this done to me, in 1981 or so at the University of MD. They decided to teach some kind of "theory of proving programs correct" to a bunch of CS-101 types who were just learning Pascal, too. I guess the hope was that we'd get a healthy dose of mathematical proofiness and write better programs.
One of our first lectures: "Taking this loop, we prove by induction that it computes the sum of the first ten integers. Here are a bunch of logic formulas (lots of scribbles on the overhead). Here's a bunch of notation, it's got CONJUNCTION and DISJUNCTION and COMPOSITION and so forth. By inference [and some hand-waving] this five line program computes a sum, yes?"
Class: "Huh?" Not even panic, just a collective, bug-eyed "<I>What the fuck?</I>?"
The approach failed miserably; what it /did/ successfully teach was cynicism; most of the students were really upset at the obvious nonsense. [I was the only one of about 250 students to complete all the project work . . . and I cheated by writing the project in LISP, and writing a LISP interpreter in Pascal]
http://www.dadhacker.com/blog/?p=755