Formally Verifying Industry Cryptography
computer.org
computer.org
That said, I'm all for anything that results in more appreciation for mathematical rigor in programming. It's like puling teeth trying to get colleagues to use tools/languages that help with reasoning about code (even just a good type system), and for a lot of programmers math seems to be an unapproachable alien language.
One thing I'd like to change about the software industry is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program. The misconception there is that the all of the program's behavior needs to be specified in order for formal verification to be useful. Why can't gradual formal verification be a thing?
I think the “middle ground” between things like typing and things like fully specified programs are things like CDK apps which hook IAM policy or network reachability tools to analyze your infrastructure (and, eg, exclude open ports on the backend).
Which is slowly happening, eg AWS or Prime Video.
is the perception that formal verification is too hard to do in practice because you can't even write down a complete specification for the program
I think the main problem is that it's too formal. Turning something that is really about simple logical deduction into thick abstract maths is sure to dissuade the majority of the people who might find it useful. The elitist gatekeeping attitude that cryptographers tend to have doesn't help either.
For system reliability at scale, I think that stronger type systems and systematic testing techniques are probably the best choice. Anyway, that puts the system in a much better state if you want to apply formal verification later.
If I remember correctly my university used to offer a "software engineering" degree, which was a real engineering degree (in the sense you could take the professional engineer exam at the end of it) and had a number of common courses with the software development degree - the focus being on system engineering, low-level programming for embedded devices, and so on. I believe it was a mix of software dev and mechatronics or electrical engineering (?) and was aimed at students who wanted to work in medical, aerospace, and similar safety-critical fields.
But I can't see it listed on the current course offerings and suspect it has been discontinued - I think it was pretty unpopular due to the requisite math courses and generally having the same level of rigour as the other engineering degrees.
Although the degree was very much a Bsc, I don't think getting a Beng was an option.
Do you see formal verification as a relatively promising niche to get into? If so, what areas (among theorem proving, model checking, static analysis, type & effect systems, etc)?
The downside is that the space is quite fragmented and a lot of tools have a high skill bar. If I was starting out, I'd probably focus on static analysis (eg. Infer or something similar - https://github.com/facebook/infer) because those tools tend to be easier to learn, and they have the potential to scale to really big systems. In contrast, Coq is a fine tool, but most people learn it by going to grad school which isn't useful short term career advice.
There are lot of great interviews with practitioners on the Galois podcast, Building Better Systems - that might be a good place to start exploring: https://www.stitcher.com/show/building-better-systems
I started learning a little bit of Lean from the Natural Number Game, and subsequently worked through Logical Foundations (with the generous help of one of the coauthors!), and have continued learning Coq afterward.
Are there books or sites or exercises out there for "people who've already learned Isabelle and now would like to learn Coq", "people who've already learned Coq and now would like to learn Lean", "people who've already learned Coq and now would like to learn tools and frameworks for verifying protocols", "people who've learned OCaml or Haskell and now would like to learn Coq", etc.?
It does look like Idris helps make it especially straightforward to write correct code and know when you've done so.
When I graduated there were some interesting opportunities, but the field looked a bit too stale and I ended up moving into a slightly different research area (probabilistic model checking and probabilistic inference in general).
There is a lot of hype around theorem proving, particularly with dependent types. As you say static analysis (and model checking) might be a better bet due to scalability, unless transformer architectures get to the point where writing proofs can be done much faster? What do you think about more practical approaches such as Dafny?