Info
Among TLA+ experts, the word "prove" means to write a formal proof and check it with the TLA+ Proof System (TLAPS). We don't do that at MongoDB, we just model-check our TLA+ specs. So let's avoid saying we "prove" our specs are correct, we only "check" them.
Top User Comments
xgen-internal-githook commented on Fri, 22 Nov 2024 22:46:04 +0000:
Author:
{'name': 'A. Jesse Jiryu Davis', 'email': 'jesse@emptysquare.net', 'username': 'ajdavis'}
Message: SERVER-97559 Don't say we prove our TLA+ specs are correct (#29488)
GitOrigin-RevId: 27a5342a5e0c92458c3447b4a0739aae82cd8809
Branch: master
https://github.com/mongodb/mongo/commit/7c982b82dfa91d5e5597359adf86ca43f6e67cd9
