3 ms·
I wish projects like this would publish their proofs with their protocols. It's interesting to be sure but I find all of the prose and diagrams to be too verbos
by agentultra 8y ago
I wish projects like this would publish their proofs with their protocols. It's interesting to be sure but I find all of the prose and diagrams to be too verbose. I'd much rather read the mathematical model of the transaction protocol.
- jchrisa 8y agoYou can read the paper that inspired the FaunaDB transaction protocol here: http://cs.yale.edu/homes/thomson/publications/calvin-sigmod12.pdf http://cs.yale.edu/homes/thomson/publications/calvin-sigmod1... Or if you want a very concise description, see slide 13 from Daniel Abadi's presentation: https://www.slideshare.net/abadid/the-power-of-determinism-in-database-systems https://www.slideshare.net/abadid/the-power-of-determinism-i...
- agentultra 8y agoThanks for the links! I meant the actual proof or model they use to verify the protocol. Is the FaunaDB team using TLA+, Coq, Lean?
- mmysteryy 8y agolol