[ngruhn]

You can write "formal" proofs in this language for mathematical theorems. They are "formal" because they are so detailed that they are machine checkable. That's in contrast to the "informal" pen and paper proofs that people normally produce.

Besides pure maths you can also use that to verify the correctness of software. E.g. say you implemented a shortest path algorithm:

   shortestPath(graph, start, end)

You could proof something like: For all `graph` and each `path` in `graph` from `start` to `end`:

    path.length <= shortestPath(graph, start, end).length