One should probably also mention functional programming languages based on some form of [typed lambda calculus](https://en.wikipedia.org/wiki/Typed_lambda_calculus) such as [Haskell](https://www.haskell.org/). 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](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_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](https://coq.inria.fr/).


----------

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][1]

    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.

  [1]: https://www.indiana.edu/~knotinfo/descriptions/pd_notation.html