What I'd really like is a way to express code in a medium/high level language, and provide hand-optimized assembly code alongside it (for as many target archite

What I'd really like is a way to express code in a medium/high level language, and provide hand-optimized assembly code alongside it (for as many target architectures as you need). For a first-pass, you could machine-generate that assembly, and then manually verify that it's constant time (for example) and perform additional optimizations over the top of that, by hand. The "compiler"'s job would then be to assert that the behaviour of the source matches the behaviour of the provided assembly. (This is probably a hard/impossible problem to solve in the general case, but I think it'd be solvable in enough cases to be useful) To me this would offer the best of both worlds - readable, auditable source code, alongside high-performance assembly that you know won't randomly break in a future compiler update.