The paper addresses teaching programming as a sequence of derivations from one partial solution to another, maintaining correctness of the partial programs at each step. This is contrasted with developing a program first, and then proving the completed solution. This approach is not a new idea, as the referenced literature makes clear, but it is applied here in the context of a second-year course, thus giving the opportunity to introduce formal aspects early in the undergraduate curriculum.

Since the authors have taken this approach with several classes of students, they have gained some knowledge about the common difficulties that students have with it. These are difficulty in understanding formal logic, not checking the conditions under which a transformation is applicable, long derivations leading to student frustration, attempting too large a step from one version to the next, omitting bounds on new variables, forgetting to carry out some proof details, and having difficulty organizing the derivation. Based on these observations, they have devised an interactive tool that ensures that the appropriate steps are taken. The developed system feeds a theorem prover that verifies the proof.

While the paper was written soon after the tool was made available to students and thus there is not a great deal of experience to support a strong conclusion, students have responded positively for the most part. The authors declare themselves to be overall “quite happy” with the tool’s use and they plan to enhance and continue to use it.