> ParticleDB’s home page advertised that ParticleDB was “formally proven” with a TLA+ proof.

Perhaps they meant formerly, probably just a speech to text problem

lumost 6 hours ago | parent | next [-]

TLA+ doesnt prove the code. if they never read the proof, then how do we k ow that it proved the right things?

	▲	hibikir 6 hours ago \| parent [-]
		And you still have to make sure all the real constraints are in. I had to fix a proven correct distributed algorithm that just happened to believe updates were done atomically and with no latency.

wavemode 6 hours ago | parent | prev [-]

lol, reminds me of the common misreading "provably safe" / "probably safe"