Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I'd hope they find themselves one or more with a master in math on logic proving in ways that a computer can help, and actually prove that their code, at least if compiled to LLVM bytecode, is adhering to the high-level architectural proof. Considering that they'd only need to prove consitency, nothing more, and especially not every little piece of code they are writing, but just the core that handles transactional isolation, not even that the code actually resolves in all cases (being stranded with a stuck cluster that is made to handle a hard reboot without problems is better than a cluster that silently violates constraints), it should not be an infeasible goal.

The main issue is that distributed database consistency without trivial, performance-killing locking schemes is too complex to prove when writing or using any trivial, local methods based on e.g. SMT solvers or so.

If something like cockroachdb would be proved-consistent on that level, it would be used for applications currently employing pessimistic locking due to a lack of trust in their database, or scaling vertically without really needing to (there are cases which make horizontal scaling cost-prohibitive due to the dependency chains in the algorithms that can solve them, but they can be replaced most of the time).



it should not be an infeasible goal

There's been a lot of work on both of these problems, but right now, proving concurrent algorithms correct, and proving equivalency of those algorithms to executable code, are very much open research problems.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: