Comment by mdaniel | Hacker News Reader

Comment by mdaniel | Hacker News Reader

Parent Full thread

As sibling comments have said, "if you rollback none of your updates will be visible" is a claim but Jepsen is designed to prove such a thing. Same with the claims of transactional behavior, and claims of Serializable

My _personal_ opinion is that databases written in footgun languages need more formal verification of claims, not less, but I guess one needs to also take into consideration the size of the audience who would be impacted by any mistake when deciding if it's worth the investment or not

---

Please don't use link shorteners on HN; we're adults here and are capable of seeing long URLs, whereas link shorteners (a) die (b) obscure the destination

https://en.wikipedia.org/wiki/Sparse_matrix#Compressed_spars...

This is actually a very good point and unfortunately formal verification is not the current norm when developing DMBSs or complex systems software. If you asked how do you know DBMS X is correctly implementing snapshot isolation, no one will be able to provide a lesson for you. This is true for every system out there I'm aware of. This goes more deeply actually about questions like this: "how do you know you implement SQL or Cypher correctly". In fact, we can't even sometimes very formally answer "what is the meaning of this query X". Back in the day my PhD advisor Jennifer Widom, who had a background in programming languages, talked a lot about how we put DBMSs into everywhere, e.g., planes that are flying up in the air, yet we can't really precisely state what the outputs of queries should be. She had some excellent writing on this for implementation of triggers that were coming out of different groups. She was one of the pioneers of triggers before triggers existed in SQL. And as I assume you might know better than me, Leslie Lamport is known as a pioneer in the distributed systems space for formal verification of programs.

Your comment on shortened URLs is noted. This is my first HN post ever :), so I might need to pick up the customs.

provide a lesson -> provide a proof.

Reply on news.ycombinator.com