This is a bit silly. Security is a chain that is only as strong as its weakest link. For decades we believed that C was the weakest link, and now, with Spectre, we have discovered (drumroll, please!): nah, C is still the weakest link. For all the amazingly scary things that Spectre brings to the table, it's still less scary than Heartbleed and Cloudbleed were.
Don't get me wrong, hardware still sucks (and with Intel and AMD's growing body of management engine incompetence they may yet overtake C as the weakest link in the chain) but we will learn from this and get better. In the meantime, we need to be pushing forward on all fronts: hardware security, language security, kernel security, application security, network security... nobody gets to stand still.
https://crypto.stanford.edu/~dabo/papers/ssl-timing.pdf
And even if C is the weakest link, all that means is that you're totally screwed. No amount of Rust will save you when the Linux kernel, your relational database, and every router between you and the attacker are written using C or assembly.
At the end of the day, if you want strong security assurances you need to prove the correctness of all the semantics (of which memory bounds constraining is but one small aspect) of every piece of software in your stack, or at the very least all the most critical pieces. And the best tooling for that is for Ada and C.
I'm probably biased, but in my experience the people actually pushing for correct-by-construction tools tend to be acutely aware of the limitations of their approach, especially when it comes to having to trust hardware to do what it says. For example, all of the people I've seen advocating for seL4 tend to be very transparent that their proofs assume hardware correctness and that they don't think it's realistic to exclude much of the hardware from the trusted computing base. Further, it seems to me that the Rust developers have been extremely pragmatic about what is possible to mitigate and what they have to trust the hardware for.
I'm sure there are some examples of what you're describing, but without any sort of references, the generalizations you're making have a whiff of bad faith.
Um, Rust and Haskell aren't about security against malicious attackers exploiting hardware/system flaws. They are about correctness against programmers writing (some classes of) bugs by mistake. The two aren't directly related. Program correctness is a worthy goal even if it doesn't protect you against hardware problems.
Same goes for the proponents of formal stuff like Coq. Even worse, because those languages are so insufferable that they induce design errors, the number of which will grow each time a poor soul will have to maintain the... thing. Then, all right, there is no mistake, the result maps perfectly to all your design errors.
> when in fact most of the serious information leakages do not originate from such problems
We've already established that the parent post made a mistake in thinking FP is about safety against attackers / information leakage. Why are you still talking about this?
> because those languages are so insufferable that they induce design errors
[citation needed]
What's your actual experience with these languages?
Yes, but safety is safety. The point of the article is that the assumption on the part of language nerds for the past few decades -- that correct choice of processes and implementation patterns as expressed by whatever favorite runtime the author wants can protect us from security bugs -- turns out to be FALSE.
Rust and Haskell programs are subject to Spectre attacks just as badly as K&R C ones from 1983. All that pontification didn't actually work!
The point is that it puts a limit on pedantry about "correctness". That's all based on an idea about a "computer" being an abstracted device, when it turns out the real-world machines are in fact leaky abstractions. The lesson to my ears isn't that you shouldn't use Rust or whatever, but that some humility about the boundaries of "correctness" would probably be a good idea for many of the pontificators.