# Programming and Proving with Total Functions

The core design philosophy of F* is that the type of a term (a program
fragment) is a specification of its runtime behavior. We write ```
e :
t
```

to mean that a term `e`

has type `t`

. Many terms can have the
same type and the same term can have many types.

One (naive but useful) mental model is to think of a type as
describing a set of values. For instance, the type `int`

describes
the set of terms which compute integer results, i.e., when you have
`e : int`

, then when `e`

is reduced fully it produces a value in
the set `{..., -2, -1, 0, 1, 2, ...}`

. Similarly, the type `bool`

is the type of terms that compute or evaluate to one of the values in
the set `{true,false}`

. Unlike many other languages, F* allows
defining types that describe arbitrary sets of values, e.g., the type
that contains only the number `17`

, or the type of functions that
factor a number into its primes.

When proving a program `e`

correct, one starts by specifying the
properties one is interested in as a type `t`

and then trying to
convince F* that `e`

has type `t`

, i.e., deriving `e : t`

.

The idea of using a type to specify properties of a program has deep
roots in the connections between logic and computation. You may find
it interesting to read about propositions as types,
a concept with many deep mathematical and philosophical
implications. For now, it suffices to think of a type `t`

as a
specification, or a statement of a theorem, and `e : t`

as
computer-checkable claim that the term `e`

is a proof of the theorem
`t`

.

In the next few chapters we’ll learn about how to program total functions and prove them correct.