Comment by ofrzeta
6 days ago
What does LaTeX have to do with TLA+? Also I think "most of distributed systems such as AWS" might be an exaggeration. At least the public known examples of formal verification in AWS are scarce.
6 days ago
What does LaTeX have to do with TLA+? Also I think "most of distributed systems such as AWS" might be an exaggeration. At least the public known examples of formal verification in AWS are scarce.
I think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.
AWS talk about it a fair amount, although rarely in a lot of detail.