Tauto という言語

この本は、Tauto の文法を初めて学ぶ人が、値と関数から出発して、所有権・代数的効果・依存型・定理証明を読み書きできるようになるための入門書です。章を順に進められるように構成しています。

対象読者は、ほかのプログラミング言語で変数・関数・if 式を一度でも使ったことがある人です。Rust や形式証明を知っている必要はありません。難しい章は、最初は流し読みでも構いません。

時間が限られる場合は、第 1〜5 章 → 第 7〜9 章 → 第 13〜15 章 → 第 20 章の順に読んでください。そのあとでタクティク・依存型・検証済みプログラムに進むと理解しやすくなります。

この本の前提

本文のコードは、次の 2 種類に分かれます。

独立した小さなコード：ファイルに保存して、そのまま動かせます。コードブロックにファイル名を付けています。
抜粋：標準ライブラリの関数・補題・構文マクロを使うものです。それらを読み込んだプロジェクトの中に置く前提です。その場合は、冒頭の import と、前の章で定義した関数を示します。

この本で大切にしたのは、次の 3 つです。

Tauto は、プログラムと、そのプログラムの性質を説明する証明を、一つの言語で扱うための言語です。普段は関数を作り、条件分岐を書き、データを操作します。必要な場所では「この関数はどの入力でも、こういう結果を返す」という主張も、コードとして書きます。

次のコードは、Tauto の二つの面を示します。

answer.taut

import std::Base

let answer := 6 * 7
perform show("答え", answer)

theorem two_plus_two(): (2: Nat) + 2 = 4 {
  Refl
}

実行結果

✓ theorem two_plus_two : 2 + 2 = 4

答え = 42

前半は値を計算し、show という操作でホストに出力を依頼しています。実行すると、次のように表示されます。

答え = 42

後半は「自然数の 2 + 2 は 4 に等しい」という命題に、証明を与えています。(2: Nat) + 2 = 4 は真偽値ではなく、証明すべき型です。こちらは tauto check で検査します。

ok      answer
ok      two_plus_two

Tauto の基礎には、普通のプログラムを記述する層と、依存型・命題・証明を記述する層があります。前者の言語的な部分を Nib と呼びます。

重要なのは、「型が合う」ことと「期待する仕様を満たす」ことは別だ、という点です。fn f(x: i64): i64 と書けば型は分かりますが、f がソートする、暗号として安全だ、メモリリークがない、といった性質までは自動的に保証されません。

考えてみよう：関数の型だけでは表現できない性質を、自分の作ったプログラムから三つ挙げてみてください。