[Crypto] Benefits of functional programming languages
Solution 1:
These languages have no side effects
Well, yes, kind of. They also are higher level languages, where you don't have (as much) control over e.g. timing or the wiping of memory. Those are the side effects that cryptographers worry about - rather than the mathematical side effects that you are alluding to.
I was wondering if those programming languages would have any benefits over "normal" programming languages when used for cryptographic applications.
Personally I think that any higher level language that provides e.g. memory protection is really a requirement for a secure application. Those kind of memory protection is generally provided by functional languages. It is probably even better than higher languages where you may have mutable variable values.
However, for the cryptographic primitives it makes sense to use machine code and - of course - native instructions whenever they are available. I've seen that bit-ops are generally much slower on these kind of languages. And we're talking about huge numbers here. For instance, Java and C# are already much slower than C if cryptographic primitives are programmed correctly (think a change of 2 x in performance degradation). Most other interpreted languages are much slower than that.
The performance advantages that functional languages may bring - such as delayed execution by passing functions - are not helpful - if not outright dangerous - for cryptographic primitives.
I was wondering if those programming languages would have any benefits over "normal" programming languages when used for cryptographic applications. Is that the case? If yes, why aren't they used more frequently?
Here again we must make a distinction between "cryptographic applications" and "cryptographic primitives". I think that a well tested library of native functions is quite often used within higher level languages. There are e.g. many OpenSSL wrapper libraries in use within higher level languages such as Python. I think this makes sense, although more (array) boundary testing on the used native libraries would be useful.
As for functional languages: I don't see this "proven correctness" as much of a benefit. Unusually there some boundary checks etc. to be made. But otherwise, generally you can work with the test vectors to show enough correctness for the primitive.
I still see purely functional languages mainly useful for mathematical applications and such like. Personally I think that they are complex enough that most developers will not use them for generic applications. Those kind of mathematical applications are generally not the type of applications that require a lot of security.
Whatever you think of the last section (which is rather opinionated), generally we don't choose a language based on the cryptography we tend to use. Security should be an integral part of an application design, but usually it is not the main use case. A language is mainly chosen because it fits the main use case or - of course - simply because of developer familiarity (and purely functional languages still are not the most popular languages out there).
Solution 2:
Functional programming languages are typically strongly typed. This makes it impossible to commit a wide class of errors when implementing cryptographic algorithms. For example, if a cryptographic key is declared as having type Word32 in Haskell, then it is impossible to add it to a plaintext of type Integer (unbounded size): the code will be rejected by the compiler at an early stage after it fails to type check.
More impressively there is the domain specific programming language Cryptol built on top of Haskell that extends the type system to allow very precise specifications of cryptographic algorithms. For example, on the main page of the Cryptol website the SHA-1 hash function is defined, with type signature
f : ([8], [32], [32], [32]) -> [32]
indicating that the $t$-th step of SHA-1 is a function $f_t$ taking three 32-bit words and returning a new 32-bit word. From the [8] we know there are at most 256 steps. (In fact there are 80.) Of course this is only the type signature, but the implementation is similarly concise.