Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct.
Proofs of correctness are a (big) step in the right direction, but they're not a silver bullet for building a secure implementation.
Heartbleed was not a side-channel attack. It was not a subtlety of the TLS specification. It was the single most well-known, common C-based security flaw. Better languages may not solve everything but they are absolutely the solution to this class of errors.
Similar could be said for Goto Fail and the GnuTLS bug. I wonder how something like Coq could handle the Debian random number bug, though. Still, 3 out of 4 ain't bad.
Do any functional or logic programming languages or libraries have a concept of entropy, and entropy generating/reducing operations?
You can use mathematics to prove other things as well. You could e.g. use a special bool type for all secure data that you can't branch on, so that no secrets could be exposed by examining the runtime path of execution. Or build a model of your CPU's caching and prefetching behaviour and prove that you're code doesn't expose any secrets by that channel.
Right--this will work on some types of side-channel attacks. For example, I could prove that my decryption function runs in a constant amount of time no matter the input.
However, you can't proactively defend against side-channel attacks. By definition, a side-channel attack exists because the designer didn't know that the cryptosystem leaks information when (s)he designed and proved the correctness of the implementation.
Proving that the cryptosystem doesn't leak information is damn nigh impossible, and often outside the scope of software engineering. My favorite example is acoustic analysis (https://www.cs.tau.ac.il/~tromer/acoustic/). Before this was shown to be possible, how were cryptosystem designers supposed to know to defend against it?
The best we can do is come up with and formalize a threat model, and then prove that the cryptosystem is secure against the adversaries in the threat model. The problem is that threat models don't help you with adversaries in the future, who have means of getting information from your cryptosystem that you didn't think of.
I take your point, but I don't think _anything_ can defend against unknown attacks. However, we could defend against all known attacks using formal methods, which is a lot better than we're doing at the moment. Further, when a new attack becomes known, I would wager that having something that is verifiable today will be easier to verify or fix in the future, as compared to a code-base that is not provable.
Just because we can't achieve theoretical perfection, we should not rule out using methods that would solve many of the actual problems we encounter today.
Of course, if you can find a way to defend against unknown future problems, I'm all in favor of using your method!
But the ideas of trusted OS and instruction might be necessary to compartment secrets to reduce their potential exposure to the least possible opportunity. It's basically impossible to completely eliminate plaintext and secrets in clear unless maths allow it, but we should still try.
TLS has so many features that it factorially increases the attack surface to the size of the Milky Way.
A much simpler nonrepudiated authenticated encryption scheme implemented in a safer language would be an ideal way forward. It also would help to have a reference implementation and reference test suite to lock down behavior.
Formalizing the TLS specification and proving that an implementation is consistent with it only shows that the implementation is logically correct. However, it does NOT show that the implementation is secure. Your implementation can be vulnerable to side-channel attacks (particularly timing attacks) while still being logically correct.
Proofs of correctness are a (big) step in the right direction, but they're not a silver bullet for building a secure implementation.