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