I've been hearing about formal methods and provable specifications as long as I've been programming (which is going on 30 years now), and I remain skeptical about them. This sort of thing appeals to me - I've skimmed over TLA+ and I like the appearance of mathematical formalism (after all, I spent 6 years getting a master's degree in CS, it would be nice if I could ever actually apply any of it for once), but all the examples I've ever seen take up an incredibly long amount of time to specify/prove things that are actually... ridiculously trivial, like a FIFO. Now it's entirely possible that there's something really significant here, and I just haven't invested the time to dig down into this enough to understand it, but I feel the same way about React, and it seems like everybody on the planet has spent the time and effort making sense of React and has found it worthwhile - so why doesn't anybody else seem to be applying formal methods?