> 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
TLA+ doesnt prove the code. if they never read the proof, then how do we k ow that it proved the right things?
lol, reminds me of the common misreading "provably safe" / "probably safe"
TLA+ doesnt prove the code. if they never read the proof, then how do we k ow that it proved the right things?