テーゼ：
- 十分に強力な型システム／型チェッカーを持ったプログラミング言語は、証明記述／証明検証に使える。
| 型 | 命題 |
| 型変数 | 命題変数 |
| 型定数 | 命題定数 |
| 型構成子 | 命題結合子 |
| 型の値 | 命題の証拠 |
| 計算・関数 | 証明・定理 |
| 計算・関数のプロファイル | 証明可能性判断 |
| プログラムコード | 証明図 |
| プログラミング | 証明作業 |
| プログラムを合成する | リーズニングする |
| メタプログラミング | リーズニング |
| 関数定義のボディ部 | 定理記述の証明部 |
異なる作業環境／ツールにより、まったく同じことをやっている。表現手段は：
- 自然言語（日本語や英語）
- 証明図（論理の伝統的図法）
- プログラムコード
- ストリング図（圏論的図法）
