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