最初のプログラム

この章では、プロジェクトを作り、検査し、実行します。

2.1 CLI を用意する

この本は、tauto コマンドを実行できる環境を前提にします。Tauto は開発中の言語で、配布の形はまだ固まっていません。ここではリポジトリを取得してビルドします。

git clone https://github.com/Hihaheho/tauto
cd tauto
cargo build --locked -p tauto-cli --bin tauto

ツールチェーンは rust-toolchain.toml で nightly が固定されています。初回のビルドには数分かかります。以降、tauto は target/debug/tauto のことです（cargo run -p tauto-cli --bin tauto -- ... でも同じです）。パスを通すか、エイリアスを作っておくと楽です。

tauto --version
tauto --help

tauto 0.1.0

--help には、init、run、check、test、fmt、lint、doc、goals などのサブコマンドが並びます。

2.2 Hello, Tauto!

名前は、英小文字とハイフンで付けます。プロジェクトを作ります。

tauto init hello-tauto
cd hello-tauto

生成されるのは、次の二つのファイルです。

hello-tauto/
  Tauto.eure
  src/
    main.taut

src/main.taut は、最初から次の内容を持ちます。

perform show("hello", 42)

hello = 42

show は、画面に直接 print する文ではありません。観測したい値をホストに渡す effect です。ホストがその値を表示したり記録したりします。

tauto check src/main.taut
tauto run --tote .

check は検査結果を表示します。run は、名前 hello の値 42 を観測して、次のように表示します。出力の形式は実行するホストによって変わります。

hello = 42

2.3 マニフェストを読む

Tauto.eure は、ソースの置き場所とプロジェクトの基本情報を書くファイルです。新しく作ったときの内容は次のとおりです。

package {
  name = "hello-tauto"
  version = "0.1.0"
}

src/ は暗黙のソースルートなので、マニフェストへの指定は不要です。追加のソースルートだけを additional-sources（リスト）で指定します。拡張子は .taut が基本で、.tauto も受け付けられます。関数を別のファイルに分けるときは、import "相対パス" と書きます（第 12 章）。

2.4 check と run を混同しない

• tauto check は、theorem などの証明宣言を、証明カーネルで検査します。
• tauto run は、実際にプログラムを評価します。

check は、命令的な関数の振る舞いを何でも証明してくれるコマンドではありません。たとえば、関数 fn を含むファイルを check にかけると、実行側の関数は skipped と表示される場合があります。これはカーネルで証明したという意味ではありません。プログラム側の型・effect・所有権の検査と、命題の証明検査を区別します。テストと証明は、目的が異なります。

試してみよう：perform show("hello", 42) を perform show("result", 7 * 6) に書き換えて、もう一度実行してください。