> The last five years have seen formal verification flourish in diverse industry niches
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)?
Great question! Formal methods groups in industry are growing rapidly and popping up in surprising places. Amazon's group is probably the most famous, but I think pretty much every big tech company has something going on in the formal verification / static analysis space. There's also a lot going on in blockchain. It's definitely becoming harder to hire people with FM skills, so in that sense, I think it's a great space to get into.
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.
nextos|3 years ago
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)?
mikedodds|3 years ago
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