Does TigerBeetle have a formal proof of serializability or has it been verified by the Jepsen tests? It's mentioned in the blog post and I'm curious how it fares in that department.
Cool project!
Cool project!
No formal proof at the moment either but it's something we're thinking about.
Everything is fully deterministic, time is externalized, so our simulation can run very fast and explore a lot of random permutations of events (which is quite effective: https://www.researchgate.net/publication/322133078_Why_is_ra...).
This isn’t as thorough as model-checking or proving a formalization of the algorithm, but it has the benefit of working with the real code. It is a bit less real than Jepsen (as we essentially mock all syscalls), but is quite a bit faster.
Do you have any thoughts on how working on TigerBeetle with Zig is? It seems like for a high performance DB rust would be a natural choice. And how's the development experience without a zig-analyzer?
zig-analyzer is great — much further along than I’d expected at this point. Though, I am still curious what the end game IDE support would look. https://github.com/ziglang/zig/issues/3028 is a big component of that.