3 ms·

Microsoft, Amazon, Oracle, Google, all sorts of large companies use them, and talk about it, publicly. They've all published whitepapers and resources about th

Microsoft, Amazon, Oracle, Google, all sorts of large companies use them, and talk about it, publicly. They've all published whitepapers and resources about them. Microsoft even employs Dr. Leslie Lamport who created and maintains TLA+ (among other things). Just for some quick examples: Microsoft: https://github.com/Azure/azure-cosmos-tla https://github.com/Azure/azure-cosmos-tla, https://www.youtube.com/watch?v=kYX6UrY_ooA https://www.youtube.com/watch?v=kYX6UrY_ooA Google: https://research.google/pubs/specifying-bgp-using-tla/ https://research.google/pubs/specifying-bgp-using-tla/, https://www.researchgate.net/publication/267120559_Formal_Modeling_and_Analysis_of_Google's_Megastore_in_Real-Time_Maude https://www.researchgate.net/publication/267120559_Formal_Mo... Oracle: https://blogs.oracle.com/cloud-infrastructure/post/sleeping-soundly-with-the-help-of-tla https://blogs.oracle.com/cloud-infrastructure/post/sleeping-... (note the author is a "Formal Verification Engineer", it's literally his job at Oracle to do this stuff) Intel: https://dl.acm.org/doi/10.1145/1391469.1391675 https://dl.acm.org/doi/10.1145/1391469.1391675, https://link.springer.com/chapter/10.1007/978-3-540-69850-0_8 https://link.springer.com/chapter/10.1007/978-3-540-69850-0_... Jetbrains: https://lp.jetbrains.com/research/hott-and-dependent-types/ https://lp.jetbrains.com/research/hott-and-dependent-types/ Arm: https://ieeexplore.ieee.org/document/9974354 https://ieeexplore.ieee.org/document/9974354

dfc 1y ago
Lamport+Microsoft was the first thing that I thought of when I read the comment. FWIW he retired at the beginning of this year.
nickpsecurity 1y ago
You named a few of the largest, technology companies who each have a tiny percentage of their programmers using or developing formal methods. That supports the parent's point. I'd also probably would count MS Research against that, or separately, since they're more like a University lab than a business. Labs often can run at a loss doing research on things that might not be practical. MS Research certainly has produced some practical things. Yet, what they do wont likely apply to a random, for-profit company. Very, very, few companies find this stuff practical outside hardware companies where it's easier to apply with clearer ROI. There's also uptake in both cryptocurrency space and distributed databases. Most business software won't use it because it makes no sense to.

dfc 1y ago

Lamport+Microsoft was the first thing that I thought of when I read the comment. FWIW he retired at the beginning of this year.

nickpsecurity 1y ago

You named a few of the largest, technology companies who each have a tiny percentage of their programmers using or developing formal methods. That supports the parent's point. I'd also probably would count MS Research against that, or separately, since they're more like a University lab than a business. Labs often can run at a loss doing research on things that might not be practical. MS Research certainly has produced some practical things. Yet, what they do wont likely apply to a random, for-profit company. Very, very, few companies find this stuff practical outside hardware companies where it's easier to apply with clearer ROI. There's also uptake in both cryptocurrency space and distributed databases. Most business software won't use it because it makes no sense to.