# 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.