A few years ago, I came across a paper by Lamport 6, which advocated structured proof in the teaching of undergraduate mathematics. A structured proof is written in a formal style, like a computer program. Lamport argues that such a presentation should make it easier for students to verify the logic of a proof.
Some major innovations in mathematics teaching have been unmitigated disasters, such as "new math," which introduced set theory into schools at the expense of more useful skills like algebra and geometry. The mistake was to confuse logic with "psychologic" to assume that mathematical concepts should be constructed in the students' minds in order of logical precedence. The advocates of new math bought, wholesale, the idea that at root mathematics is an abstract game played with symbols according to meaningless rules. It was a bit like teaching music by starting with the theory of harmony instead of singing songs, and it lost sight of all the aspects of mathematics that give it meaning and relate it to experience. The philosophy was reductionist rather than contextual: focused on form rather than meaning, on syntax rather than semantics.
I felt that Lamport's proposal was in danger of falling into the same trap. Its motivation seemed to be to teach students to