So we should choose the approach that gives us trivial attacks that reveal 64K straight out of Compton to the approach that may be slightly harder to defend against timing attacks?
This is such an obvious false dichotomy that I'm sure most people will notice, but I'm pointing it out anyway.
We could use something that gives both advantages, like the OCaml I already mentioned. Or, we could take a hybrid approach, where something like Haskell generates C code that provably can't have buffer problems. Or, we could statically verify that the library is written in a known-memory-safe subset of C++. Or, we could use a language like Rust, which (once it's eventually complete) seems ideal for this sort of application.
I think the "define a strict, branchless DSL" approach is the right one, if you're going with Haskell. Then use the type system to ensure that only that stuff can touch key data. No problems with laziness or timing attacks, if the core of that is implemented correctly.
We could use something that gives both advantages, like the OCaml I already mentioned. Or, we could take a hybrid approach, where something like Haskell generates C code that provably can't have buffer problems. Or, we could statically verify that the library is written in a known-memory-safe subset of C++. Or, we could use a language like Rust, which (once it's eventually complete) seems ideal for this sort of application.