4 ms·
Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.
by jackblemming 10mo ago
Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.
- AlotOfReading 10mo agoSeL4, a number of mathematical theorems, a bunch of cryptography. You've likely trusted your life to compcert. It's not nothing, but it's admittedly a bit limited. Formal methods are the hardest thing in programming, second only to naming things and off by one errors.
- atomicnature 10mo agoLeslie Lamport built latex, most of distributed systems such as AWS services depend on formal verification. The job of Science here is to help Engineering with managing complexity and scale. The researchers are doing their jobs
- ofrzeta 10mo agoWhat 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.
- MangoToupe 10mo agoI think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.
- justincormack 10mo agoAWS talk about it a fair amount, although rarely in a lot of detail.
- scrubs 10mo agoI see no need to dunk like that. There are ample stories over the years on HN how software orgs without using FM have bugs, waste money, treat people poorly, all leading to canceling software projects before delivering anything to customers. And I'm only mentioning just a very few issues. Software development in corps has many challenges to ROI and customer satisfaction. I might also point out FM had a nice history of value-add in HW. And we know HW is higher quality than software.