Your First Program

In this chapter, you will create a project, check it, and run it.

2.1 Set up the CLI

This book assumes that you can run the tauto command. Tauto is under development and its distribution process is still evolving. Here we build it from the repository.

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

The toolchain is pinned to a nightly release in rust-toolchain.toml. The initial build takes a few minutes. In the rest of this chapter, tauto means target/debug/tauto; cargo run -p tauto-cli --bin tauto -- ... works too. Adding the executable to your PATH or defining an alias makes it easier to use.

tauto --version
tauto --help

tauto 0.1.0

--help lists subcommands such as init, run, check, test, fmt, lint, doc, and goals.

2.2 Hello, Tauto!

Use lowercase English letters and hyphens for the project name, then create the project:

tauto init hello-tauto
cd hello-tauto

This creates two files:

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

The generated src/main.taut starts with:

perform show("hello", 42)

// Observe a value through the host rather than printing directly.

hello = 42

show is not a statement that directly prints to a screen. It is an effect that hands a value to the host for observation. The host may display or record that value.

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

check reports check results. run observes the value 42 under the name hello and displays something like this; the exact format depends on the host:

hello = 42

2.3 Read the manifest

Tauto.eure describes the project and its source layout. A newly created manifest looks like this:

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

src/ is an implicit source root and does not need an entry in the manifest. Use the additional-sources list only for extra source roots. The usual source extension is .taut; .tauto is also accepted. To split functions across files, write import "relative-path" (Chapter 12).

2.4 Keep check and run distinct

• tauto check checks proof declarations such as theorem with the proof kernel.
• tauto run evaluates the actual program.

check does not prove every behavioral property of an imperative function. A file containing fn declarations may report those functions as skipped, which does not mean that the kernel proved them. Distinguish checking program types, effects, and ownership from checking proofs of propositions. Tests and proofs serve different purposes.

Try it: Replace perform show("hello", 42) with perform show("result", 7 * 6) and run the program again.