One should probably also mention functional programming languages based on some form of typed lambda calculus such as Haskell. There is quite a bit of category theory going on in the type systems of these languages which can be familiar ground and an exciting application of their mathematical knowledge for a lot of mathematicians.
Moreover, Curry–Howard correspondence says that "types are propositions" and "terms are proofs", so one could argue that programming in such languages is the same as proving theorems. This approach is especially prevalent in dependently typed languages such as Coq.
But perhaps you're not a category-theorist or logician (or at least don't think of yourself that way). That's okay - languages like Haskell are still a great way to set up mathematical computations. This is because in Haskell, describing to the computer how to do computations is generally very similar to describing to other mathematicians how to do the same computations!
As an example in low-dimensional topology, consider the following code fragment from http://katlas.org/wiki/The_Kauffman_Bracket_using_Haskell, which computes the Kauffman bracket of a knot diagram specified using PD notation
kauffman :: PD -> R
kauffman [] = one
kauffman (Join a b:pd) | a == b = (-av*av-ai*ai) * kauffman pd
kauffman (Join a b:pd) | otherwise =
kauffman (map (fmap (\c -> if (c == a) then b else c)) pd)
kauffman (Cross a b c d:pd) =
ai * kauffman (Join a b:Join c d:pd)
+ av * kauffman (Join a d:Join b c:pd)
The last four left-aligned lines give four definitions of the kauffman function.
The first line, kaufmann [] = one is a base case specifying the Kauffman bracket of the empty diagram. The second line is the rule for eliminating disjoint circles, and the fourth line is the crossing axiom. (The third line handles some technicalities in PD notation.)
If you've ever seen a talk on the Kauffman bracket (or the Jones polynomial) you've seen these three axioms, and they're just about all we need to tell Haskell to get it to compute Kauffman brackets! So there's obviously something very appealing to mathematicians going on here.
For the curious, some specific features of Haskell (which are common among statically-typed functional languages) that enable this programming style are:
- lazy evaluation;
- type polymorphism;
- treating functions as first-class values; and
- a good algebraic data type system.
