Whenever you look closely at what these proof nerds have actually built you typically find… nothing. No offense to them, it’s simply reality.

▲

scrubs 3 days ago | parent | next [-]

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

▲

AlotOfReading 3 days ago | parent | prev | next [-]

SeL4, 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 3 days ago | parent | prev [-]

Leslie 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 3 days ago | parent [-]

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.

	▲	MangoToupe 3 days ago \| parent \| next [-]
		I think the implication is that Lamport is a proof nerd, not that LaTeX has a direct relationship to proof software.
	▲	justincormack 3 days ago \| parent \| prev [-]
		AWS talk about it a fair amount, although rarely in a lot of detail.