>But they where harder to implement and very complex
This is the general trade off for being correct. Being mostly right is easy, but leads to complex security issues later. Being correct is very hard, but should reduce the number of flaws to a manageable level.
I think Lean or Ada would be examples of different types of correctness contracts.
I remember those languages were used to verify an implementation, in space rockets code (uni teacher said). But maybe there is a way to build something perfect instead of veryfying the correct implentation?
There are two different layers here. You have the binary layer, where software is written and works at on a theoretical level. Then you have the messy components that interact with reality at an analog level. This is why one of the first tenants of security is don't give anyone else access to your hardware.
But even that isn't a foolproof winning strategy. When you start digging deeply you realize we exist in the allegory of platos cave. The reality we experience is an emergent phenomenon related to the scale at which humans operate. Things that operate at a much smaller scale experience a completely different reality than you do. For example gravity becomes so insignificant it's like it doesn't even exist when you're small enough. At least for me it's not hard to imagine nano machines that infect the substrate of a CPU and farm all your secrets out on side channels, or any number of other things that are pure sci-fi at the moment.
