I've been teaching inductive proofs of code correctness to high school students for three years now, and the instruction has steadily improved. Many of the students come in not having done inductive proofs in math yet, so it takes some time to teach this.
As of this year, the large majority of my students are writing virtually 100% correct proofs for algorithms that they have never seen before. However, this takes a large amount of class time (many weeks), and it has become a box-ticking exercise that the students are not excited by. This is certainly not what I want.
Here are a list of some of my personal favorite takeaways from this unit:
- You are proving an infinite number of things using a finite amount of ink.
- We normally conceptualize our variables as just that: variable. But really, they are a cascading series of constants, and the reality is that the runtime program goes sliding through these constants. We can designate these constants using subscripts. If you have a
forloop in which
iincrements from 0 to 50, $i_0$ is always 0, and $i_1$ is always 1. They're not truly variable. It's a subtle distinction, but I find it beautiful, and I also believe that it is a nice lead-in to that aspect of functional programming.
- We can make real guarantees about code in the first place.
This list has been thus-far unconvincing to my students. I need to make this unit more exciting. How do I demonstrate to my students that this is both interesting and beautiful?