[nextos]

> 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)?

[mikedodds]

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.

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

[nextos]

Thanks for your reply. I must clarify I do have a theoretical background in formal methods (a research-oriented 2-year MSc in that topic).

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?

[mikedodds]

I love Dafny - we've worked on it in the past in fact. Theorem proving is definitely something that's being applied in industry - our crypto verification project uses Coq in some places. There's definitely a lot of hype though, some of which seems a bit unrealistic to me. There's a long, long way to go before theorem proving is practical as a tool for general programming, rather than in ultra-important niches like core crypto libraries.

[schoen]

I'm curious about resources that are specifically meant to help people who've learned one proof environment learn others.

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.?

[jnash]

Have you tried Idris? It is a "practical" programming language that also gives you the full power of Dependent Types to prove your code correct. There is a great book "Type-Driven Development with Idris" that really helped me open my mind to the power of Dependent Types.

[schoen]

Yes, I'm borrowing that specific book from a friend who is really into functional programming, but I haven't read it.

It does look like Idris helps make it especially straightforward to write correct code and know when you've done so.