compilers famously love to optimize away all your code to make it execute faster without changing behavior, which is usually great news. but also, famously, sometimes the "slow" speed is the desirable behavior in cryptographic algorithms.
it is, to my understanding, generally accepted that compilers just don't understand this constraint, so it's often the case that constant-time algorithms are just written in raw assembly, because the compiler won't try to make that faster.
but like, is there any compiler that understands? is there any language where constant-time code / "no timing side channels" is at all possible to express in a way that the compiler isn't allowed to break those invariants?
by which i specifically mean: is there any vaguely high level programming language with these properties, such that "optimizations" broadly are possible, but the Dangerous optimizations can be reliably avoided when necessary to uphold security properties? not just an escape hatch to disable optimizations (or even a fine-grained way to opt out of specific optimizations). i mean a system to encode the actual invariant and where the language semantics rely on this for correctness. maybe even, if i say that a value should be constant-time but the way i wrote it has a side channel before optimizations, the compiler should reject that too, the same way as returning the wrong type of value is unacceptable.
is there any tooling that does something like this? or which otherwise knows how to reason about such code in an interesting way? to be clear, the goal is not to write crypto code. my goal is to maybe learn a novel way to reason about code.
