development. For the time being, the project consists only of
this wiki and an incomplete reference implementation (licensed
under the GPL).
Constructiva is functional, statically typed, and lazily
evaluated. Constructiva lies at a particular crossroads between
mathematics and computer science, with a long-term goal of
Constructiva's type system is richer than those of most functional
programming languages in that it supports the all the facilities
one needs to express mathematical logic. For example, there is a
type which contains exactly the prime numbers. To facilitate this,
among other things, it is possible to prove the mathematical
equality of two expressions directly within the language.
To the mathematician, Constructiva is perhaps most notable for
furthering the Constructivist program. It aims to be a suitable
system for formal proofs in Constructive mathematics. However, it
is not a general framework; it represents a specific axiomatic
system. It allows mathematicians to take full advantage of
constructivism by representing proofs in a familiar way (the
elementary logic of topos theory) and also allowing direct access
to one's constructions by incorporating them directly into
It is important to note that Constructiva is not Turing complete. It
contains no facilities for general recursive functions or unbounded
loops; such facilities would allow meaningless proofs through the use
of non-terminating constructions.