# Structured Proof Script LanguageΒΆ

Harpoon proofs are recorded in signature files as a **proof script**. This is a
structured language whose core constructs close resembles the syntax of
Proof tactics. In a signature file, a proof named `foo`

is declared as
follows.

```
proof foo : tau = P;
```

where `tau`

is a computation type and `P`

is the body of the proof.