The use of proof tools in software is very, very interesting but still a niche application because of the relative specialization of the programmer and the need

The use of proof tools in software is very, very interesting but still a niche application because of the relative specialization of the programmer and the need: most software limps by just fine with shockingly high defect rates. But, of the folks I know that do this kind of work you’re looking at critical applications in the MiC or bigger tech companies that produce their own hardware. Compilers for Important Things also fit the profile. I’m not aware of apprenticeship models. More education or building provably correct systems on your own time until you can go professional are the roads I’ve seen (but not traveled). Model checking distributed algorithms and complex systems is another path, one I suspect has more industry need than is realized. Getting over the imagination hump in an org is the trick there, yet. I hope by the time I retire proof tools are the norm. It’s heading in that direction, seems to me. When I started my career static vs dynamic was a big deal and here we are with typescript being mainstream. I do a lot of work in Rust and what that compiler can prove about lifetimes is still sometimes a surprise, compared to what I used to just have to muddle through over in my mind.