logoalt Hacker News

Powdering7082 • today at 3:46 PM • 2 replies • view on HN

> 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


Replies

lumost • today at 5:30 PM

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

➕ show 1 reply
wavemode • today at 5:40 PM

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