People who have written the axioms for math (technically, ZFC, if you know what that is) as a computer program, allowing automatic verification and the like.
* http://us.metamath.org/
Finally, here two slightly more accessible explanations which do not employ the same isomorphism, but which try to explain the same idea.
Take special note of the second one, because it has a good explanation of what math is and many people seem to have math confused with whatever they happened to learn in math class.
It is a solid argument in some cases. Consider that software is written to solve problems - this directs the choice of math needed, and choosing math is essentially what invention is. The same applies with mechanical inventions, you apply physical theories (maths) to describe or make something - the problem with software is it is unfamiliar.
The example I like is the "Carmack's" reverse shadow algorithm which famously was patented. Its easy enough to invent - I remember thinking in passing and never following up that it could be done when first reading about the "classical" broken stencil shadow implementation. It is a consequence of trivial geometric observations, and the precise operations needed are so simple that there is pretty much one best way to implement it in-terms of an algorithm. "count how many times a ray cast /to/ the camera /from/ infinity enters or exits a shadow volume before hitting the front face of the object we are shading, odd means it is in shadow, even means it is not". sure we can use stencil buffers and xor to implement it efficiently, but its still very simple. Now if we compare it with, say, some cascading shadow map solution then we do have a simple algorithm in shadow mapping "cache the distance from the light to each point in buffer by rendering a z-buffer from the light's perspective, then use the light direction to reconstruct the distance from the light in the main render - if this distance is greater than the value in the buffer then we are in shadow", but the details of the implementation are much more variable - you have a whole choice of buffer types and layouts, rendering techniques etc. and the nature of the algorithm doesn't map well to hardware making for odd things like bias and slope on depth reads/writes. In short they are much more complicated - I think they are probably patentable because the chance of me coming up with that if asked to find some shadowing algorithm with no prior knowledge is extremely low - mostly because it is a very hardware specific approach which makes no sense unless you have z-buffers etc. The Carmack approach is conversely doable on pen and paper by hand very easily... having a patent on it is madness imo because it equates with trivial, intuitive geometry that I'd bet most programmers who never heard of the problem can reinvent on the spot...
You don't need Haskell in particular btw all code is maths owing to lower level things (CPU instructions) - you don't need to convert it to anything for this argument to hold. i.e. All software is isomorhpic with a subset of math.
