Attempt to be mentioned in TLA+ homepage · Issue #5784 · tikv/tikv · GitHub
DRANK

Question I'm learning TLA+ and found there's an Industrial Use of TLA+ page recording companies who use TLA+. Since we have a TLA+ repo and posts (though in Chinese), I write a simple email...

github.com
Related Topics: GitHub Git
1 comments
  • TiKV でちょっと面白いというか、微笑ましい issue を見つけてしまいました。

    近年、分散 DB を中心に industry でも形式手法が採用されるようになってきました。形式手法は、すごく雑な説明をすると、テストではなく数学をベースにしてシステムの動作を検証しようとする分野です。中でも OSS 界隈では TLA+ というツールがよく採用されています。

    この TLA+ は大御所 Lamport の理論が元になっていて、本人も積極的にツールの普及を推進していたり、採用事例をリストしたりしています。

    https://lamport.azurewebsites.net/tla/industrial-use.html

    で、リンクした issue を見ると、要するに「TiKV / TiDB でも TLA+ を使ってるんだから Lamport のページに載せて宣伝してもらおう」ということなんですね。

    結果的には結局 issue も open のままで Lamport のページには載ってないんですが、TLA+ 側からは認知されていて、実際、TLA+ が開催しているレクチャーシリーズ Dr TLA+ で TiDB を扱った回があります。分散アルゴリズムの回が色々ある中、ケーススタディとしては TiDB は Cosmos DB と同格に取り上げられていて、割といい扱いなんじゃないでしょうか。

    https://github.com/tlaplus/DrTLAPlus

    残念ながらスライドや映像は公開されてないみたいですね。気になる。