TLA+の社内勉強会スライド公開します
Raftを使ってDFSを作るという仕事を数年前ぐらいから続けています。そのためか最近、形式仕様記述（特にTLA+）とかModel checkingとかTheorem provingとかが私の中でアツいです。TLA+とかAlloyとかVDM++とかSpin周りのやつです。
ソフトウェアの仕様を形式仕様で厳密に書き下して検証、証明するという手法がある！ということ自体は院生時代に見聞きして知ってたんですが「難しそう」とか「一部のすごい人にしか使えなさそう」といった先入観があってなんとなく敬遠してました。正直、当時は自分の身近な問題であると感じられていませんでした。
あれから10年以上たって最近形式仕様記述とかModel checkingとかTheorem provingというものは「必須なものである」という認識がようやく私の中にも芽生えたようです。仕事で分散システムの開発を通じて「これは人間の頭（複数人の設計レビューとかコードレビューとかテスト）だけではデバッグ不可能なのだ！」というのが骨身にしみてわかったからだと思います。
10年前とはちがって、Amazonでの大規模な形式仕様記述（TLA+）とModel checkingの導入による成功例なども表立って論文の形としてまとまってたりしてて、もうこれはやるっきゃ無いだろという感じです。
今はAWSとかでちょっと気の利いたサービスつくると、もうそれは分散システムになっちゃうんですよね。ここ10年間だけを切り取ってみても、ソフトウェアエンジニアが作るシステムの複雑さが格段に上がっているように見えます。
そんな中で形式仕様記述とかModel checkingとかは今後ソフトウェアエンジニアにとって必須のスキルになっていくんじゃないかなと思っています。ので、みなさんもぜひ見てみてください。
このスライドでTLA+のさわりと、TLC Model Checkerでの仕様バグの検証のやり方とか。一通りわかると思います。
あ、間違ってたらこっそり教えて下さい！
