# December 9, 2008

## Make tool, evaluate tool

One of my officemates gave a presentation of his research yesterday – and I decided to come and listen. Like me, he has an interest in CS and Math education and tools for the same. He’s got a different approach, than I do, though.

He presented a notation for formal proofs of correctness, and proposed a tool to help undergrads produce these proofs by providing available “next lines” for the proof. I cringed a little every time he said his notation was “proven consistent and complete” (If so, he’s got something bigger than a thesis project on his hands), but mostly I wanted to know why he thought it would be at all helpful. He and his adviser had a thought that it would make exploring possible proofs less tedious, and so on. Maybe, but from what I’ve read, the parts of writing such a proof that students have most trouble with are parts that are almost invisible to this tool – understanding definitions, moving between levels of formality, and so on.

It’s something that frustrates me about some CS research. You make a tool, then see if it helps. And you design the tool based on your own conceptions. My officemate is a nice guy, but he’s one of the people I know who is most into formalisms and notation. He doesn’t approach proof like most mathematicians I know, who have a more “holistic” kind of approach where they move between levels of rigour.

We took a mathematical course together last year, and I noticed that he didn’t do the same sort of “frame of reference” shifting I like to do – turn a question about codes into a question about vector subspaces or fields, or proving non-existence by contradiction (my favourite kind of proof). He really did approach proofs in a step-by-step manner, applying a known law or transformation at a time. We both did well, so I don’t want to say my approach is better. I do think, from what I’ve read, it’s more like the average mathematician’s approach – my undergrad profs must have trained me well for the discipline I’ve abandoned.

I did convince him he should read a little about mathematics and computer science education research. I put a lovely paper about learning formal proving on his desk – I’m hoping to get talking with him about it. If he is willing to consider the way learners really do think about proof, I’d love to help him develop this tool. I might have to sell him a bit more on this, though.

## Leave a Reply