← All posts tagged math


По мотивам последних срачей о хаскелле монадах и прочем у меня сложилось ощущение, что многих людей в голове стоит знак равенства между "абстрактный математический объект" и "бесполезная фигня".


Constructiva is a new programming language in the early stages
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
influencing both:

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
computer programs.

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.