# The Istari Proof Assistant

Istari is a tactic-oriented proof assistant based on Martin-Lof type
theory. It is intended for mathematical developments that involve
computation – particularly imperative computation – and dependent types.

### Overview

The Istari workflow is similar to proof assistants such as Coq: one
proves a theorem by building a *proof script*, which consists mostly
of invocations of *tactics*. Each tactic acts on a current goal, and
generates zero or more new subgoals.

Istari proof scripts and tactics are ordinary ML code, written in a
dialect called IML that is close to Standard ML. User tactics enjoy
the same access to the prover’s internals as the vast majority of the
built-in tactic library. As in some earlier proof assistants (notably
LCF), user tactics can manipulate proof objects (called validations)
and soundness is ensured using abstract types.

As Istari is based on Martin-Lof type theory, Istari’s typing
judgement is a proposition **within** the type theory, rather than an
external mechanism (as is more typical in proof assistants). This
creates advantages and disadvantages: The main advantage is there is
no distinction between definitional equality and user-established
equalities. Thus, an equality proven by the user is just as valid for
typechecking purposes as any another. For example, if `M : A(N)`

and
`N = N'`

, then `M : A(N')`

. In many proof assistants, this principle
works for definitional equalities but not user-established equalities,
which can create severe challenges when using dependent types.

On the disadvantage side, typechecking is undecidable, since it can
depend on arbitrary mathematical facts. In practice, the typechecker
usually attends to typechecking obligations, but sometimes one sees
proof goals of the form `M : A`

. Often these indicate type errors,
but sometimes they are true facts that the typechecker was unable to
prove on its own.

In contrast to many Martin-Lof type theories, Istari supports
impredicative quantification (as well as the usual predicative
hierarchy of universes). Istari is also unique in that it supports
guarded recursive types, and indeed impredicative quantification over
guarded recursive kinds. Guarded recursive kinds make it possible to
reason about imperative code that uses higher-order state.

The Istari type theory is itself formalized using a different proof
assistant (Coq), and essentially all of the Istari inference rules are
validated using that formalization.

### Table of contents: