Perhaps my experience was atypical, but freshman year included a course on proofs of correctness, starting from propositional logic and ending with LTL (comparable in concept to the system Lamport published as TLA+). Upper level course often included a hands-on section on PROMELA. These are not something I would expect a rando practitioner to know about or teach, and only rarely put into practice (albeit to good effect -- amazon uses TLA+ to formally verify their AWS services: lamport.azurewebsites.net/tla/formal-methods-amazon.pdf).

And that's really the value of an undergraduate degree: learning stuff industry hasn't yet widely adopted from the people who helped invent it.

I'm not trying to be cheeky, but you're proving the point: I'd argue that UNIX systems and tools are the foundation of AWS, not TLA+. Amazon was famous for being held together with Perl, back in the day.

If your service or company survives long enough for the marginal cost of applying TLA+ to it to be worthwhile, you can afford to hire postdocs to work on it. They probably have 10 people using TLA+ on it. There are probably 500 software engineering teams in the world that are mature enough where the payoff is worth it.

It's not to say that TLA+ isn't useful, or that it isn't worth learning. It's just that TLA+ is never going to be a bedrock tool in the same way that UNIX systems knowledge is.

> If your service or company survives long enough for the marginal cost of applying TLA+ to it to be worthwhile, you can afford to hire postdocs to work on it.

Judging from the Amazon open reqs I've seen, it's their SRE team writing TLA+. So like, both topics are useful; I just don't think it's worth paying a professor to teach you how to use computers when there are so many other resources available. This is why I support things things like LUGs and student jobs -- I spent like 5 years supervising student SREs for the OSU Open Source Lab, speaking at Barcamps, presenting and advising at LUGs, etc. And why a couple of PhD students are running a one month session and recording it for posterity.