TLA+を雑にはじめた
某犬のSVGアイコンの人にそそのかされてTLA+をはじめた。
TLA+とは何か
形式言語の一つ。AWSの一部サービスの仕様を記述し、仕様エラーや新たに機能追加する際のチェックに利用してるらしい。
DynamoDBとかS3とか2014年の時点で14のサービスがこの言語によって、仕様を記述され実際に利用されているとのこと。
https://dl.acm.org/citation.cfm?id=2699417
- 状態遷移を記述できる
- 初期値パラメータセットを集合で表現できるため、取りうる値の全てを列挙しチェックできる
- 状態遷移していく中でパラメータが変化していく中、その値が正しい範囲に収まっているかなどのチェックが可能（Invariant）
- 並列実行される処理の仕様をチェックすることができる（Concurrency）
TLA+を学ぶ
TLA+は普通のプログラミング言語とは違い、数学的な正しさを証明することで仕様をチェックできる。そのため、数学的な記号や概念が多少なりとも必要とのこと。そのため、自分のように数学あんまり得意じゃないマンには若干ハードルがあがる。しかしながら圏論やれとかそういう話ではなさそうなのでまだなんとかなりそう。
公式HPには様々なリンクが入っているのでチェックする。
まずはVideo Lectureを全部通しで確認しよう
ゆっくりやっていきます。
