- What Is Functional Programming? / Provability
- Speed
- Concurrency
- Monads

Since the mid 1980s, functional programming has been one of those things that periodically crops up as the magic bullet that will save everyone from the horrors of buggy code, or will magically make everything faster. It hasn't delivered on this promise in the past, but it may in the future. In this article, I'll take a look at why.

## What Is Functional Programming?

A lot of languages contain subroutines and call them functions. This is quite confusing. Languages like C refer to all subroutines as functions. Pascal referred to subroutines that didn't return a value as procedures and ones that did as functions.

In mathematics, a *function* is something that generates a value based on the values of its arguments. The important distinction between a function in C or Pascal and in mathematics—and in functional programming languages—is that it has no side effects. As a trivial example, C's `puts()` “function” is not a mathematical function because it writes something to the standard output.

Antoine de Saint-Exupery wrote, “Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away.” One of the interesting things about programming language design is that you can often gain more power by removing features from a language than you can by adding features. Functional languages remove two very important things from a language:

- Mutability
- Side effects

Some languages are almost-functional, but still allow side effects or still allow mutability. These languages—F# being the most notable example—manage to combine all of the disadvantages of imperative and functional programming, giving something that is not so much a functional programming language as an imperative programming language with a set of irritating and seemingly arbitrary constraints.

## Provability

The thing that makes functional languages popular with theoreticians is that we have spent the last 3,000 or so years developing tools for proving properties of mathematical expressions. Most of these tools can also be applied to a functional programming language.

Unfortunately, Go—del's incompleteness theorem has a nasty habit of biting you when you start thinking that you can prove useful things about programs. In fact, you can quite easily prove that you can’t prove any nontrivial property of program in the general case.

Fortunately, as with most other things in computing—and engineering in general—there is often a good-enough solution. This applies even to things like the halting problem. Computer science undergraduates are expected to prove that you can’t show in the general case whether a program will terminate. You can, however, prove for most programs whether they will terminate given a specific set of inputs, and you can also prove whether their inputs will be in this set. Although no general solution to the halting problem that exists, there are solutions that can be applied to specific programs, and especially ones written in functional languages, where it is easy to decompose the programs and prove properties of individual parts.