OK, so the main reason I asked this question is that I’ve been thinking about ways that a person, such as myself, who isn’t in academia, might get started learning about formal verification. I’ve begun learning coq using Software Foundations along with Coqart for a bit of deeper background material. However, I generally prefer to learn by doing, and I thought working on formal verification of some simple utility libraries might be a path that makes sense, but would prefer to avoid duplicating work that others have already done.
At this point I’m wondering if this approach even makes sense. I’ve known about HOL, Isabelle, Coq and a few others for a long time and I was under the impression that Coq was currently the most widely used/well documented of these or at least the one with the clearest accessible learning path.
However in the past few days I’ve learned about Why3 and now CakeML and I now feel more confused and uncertain about which would be the best to learn.
My general belief is that we need to get to a world where software is much more reliable and secure than it currently is and that the best path toward that goal is formal verification. But given how much software there is running the world today, it seems to me that this will likely require a much larger number of developers to become familiar with formal methods than are coming out of a hand full of PhD programs.
Are these ideas completely unrealistic ?