[agentultra]

I haven't read all of it yet but it also seems to miss the vein of development that has led to movements such as Correct by Construction et al. The idea that we should model our computations in a high-level specification and check that those designs meet our goals and hold the invariants we press upon them.

Instead there's Agile and the idea that we can throw together something that roughly works and iterate until our confidence is enough such that we can release it. The so-called, beta-driven-development. (Perhaps a vestigial remnant of the unix philosophy?).

I'm not arguing that formal methods should be used for every software project. I think Carmack was right to point out that if all software was written like the software at JPL we'd be decades behind where we are now. However I do think that it should be a part of the experience of becoming a programmer so that when we encounter hard problems we have the correct instincts to rely on mathematics to help us.

[mixmastamyk]

This is a beginners book, and keeping in mind we can't teach them everything in the first "semester," do you still think this topic should be included?

[agentultra]

Definitely think the groundwork can be laid out without covering the entire breadth of formal methods. Even a history lesson with Djiskstra, Lamport, Mizra, et al can be illuminating. It's good to lay the foundation so that when a beginner encounters a problem they have the instincts to know that they should look up these tools in order to help them.

I found it a shame that I didn't encounter these tools only until very recently. It's a well kept secret in academia that I think should be shared.