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.