TypeScript は、ワークフローのような処理を少量のコードで書けます。 たとえば「あるノードから次のノードへ進む」という処理だけなら、数十行で実装できます。 一方で、実装の規模が大きくなると、次のような不安が出てきます。 ワークフローを扱う関数の間で、ワークフローに期待する意味がずれていないか テストしていない入力で、想定外の振る舞いをしないか 実装を変更したとき、以前満たしていた性質を壊していないか この記事では、非常に小さなワークフローを題材にして、定理証明支援系 Lean を使い、TypeScript 実装が Lean で書いた基準となるモデルと一致するかを検査する方法を...

💾