mmiao

the format is not friendly at all...

imho, model checker suits for the problem with many different states and complex state transformation. But in this case, it's a simple toctou problem.. Using model checker sounds weird for me

a 100 million rows table is fairly small and you just don't need a distributed database. but you will need one if you hit 10 billion rows

Making a basic database that works is not hard, but making a robust one is really hard. What makes SQLite shines is its extensive testsuite. I still don't understand the motivation of limbo, as without years of hardwork on test you can't say you are correct, and why i should pay for it...

But we need extra computation to move forward/backward, which is not suitable for the problem