[jude-]

Secure implementations require more than formal, logical correctness. They must also not leak information to adversaries--i.e. the must be free of side-channels. Unfortunately, ensuring this usually requires the developers to be aware of the low-level behavior of the underlying architecture, which is difficult in functional languages since unlike C, they abstract away behaviors of the underlying hardware that can leak information.

I suppose you could extend the functional language's type system to tag data as e.g. needing to be compared to other data in constant time, or needing to be accessed in a particular way to avoid cache-timing attacks, and so on, but this just off-loads the problem to the compiler (i.e. the problem must still be addressed, and not in a high-level functional language). But if you're going to go that far, you might as well put the requisite safe code primitives into a shared library, so if you find bugs in them later (or discover new side-channels you didn't think about earlier), you can update the library without having to re-compile and re-deploy everything affected by it.