I'll get around to delving into both of these topics eventually just for fun, but I'd like to know what HN thinks of its usefulness beyond intellectual curiosity. I don't remember where, but I've read online comments claiming that TLA+ can really change and improve the way one thinks about software design, and that it's made to be used in regular dev jobs. And I bet there's something to gain from learning how to use Coq, even if I never use it in my day job.

I know this will cause some eyerolls, but I do wonder how this will all fit into a future way of software dev where most of the code is written by AI based on simple pseudocode, as the next form of "high level" programming. There was an interesting discussion about this [2] a few days ago.

[0] https://softwarefoundations.cis.upenn.edu [1] https://lamport.azurewebsites.net/tla/tla.html [2] https://news.ycombinator.com/item?id=39934956