TiDB 2.0 Is Ready – Faster, Smarter, and Battle-Tested | Hacker News Reader

TiDB 2.0 Is Ready – Faster, Smarter, and Battle-Tested

pingcap.com

58 pointsgregwebs10 comments

Their site/domain seems to be having issues so here's a direct link to the blog post on github pages:

https://pingcap.github.io/blog/tidb-2-0-announcement/

So, they greek all the text on the page unless you turn on Javascript, but even if you turn on Javascript for their own domain, they still greek all the text?

I'm confused. Why would they want to do that?

> To ensure correctness in our design and implementation, we use TLA+ to formally prove our work.

Hah, I'm sure it's not for the whole thing but I wonder how many vendors can claim anything close to that!

Fwiw, they've open sourced their TLA+ proofs for percolator and raft merge. Worth checking out: https://github.com/pingcap/tla-plus

Both Microsoft (Leslie Lamport's current employer) and AWS, at least:

https://en.wikipedia.org/wiki/TLA%2B#Industry_use

Seems like good company to be in.

That Lamport and his current company are using TLA+ does not surprise me ;-) AWS is interesting. Before jepsen and similar stuff we used to have to take the vendor's word on a lot of claims. Hopefully the attitude there is changing towards more public self-verification (releasing stuff this) and then independent external verification!

I've been watching this project for a while, it seems pretty interesting. Does anyone here have experience operating this in production?

Take a look at the third paragraph with links to accounts from Mobike (bike-sharing) [1] and Yiguo (fresh food deliver) [2].

[1] https://www.pingcap.com/blog/Use-Case-TiDB-in-Mobike/

[2] https://www.datanami.com/2018/02/22/hybrid-database-capturin...

Did I miss some development in networking theory? Seems popular to claim infinite horizontal scalability these days, and last I checked that's somewhere between hyperbole and a violation of physics (aka lying).

Reply on news.ycombinator.com