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