I looked for pretty much the same, and it seems that if you don't use problematic features, you should get closer to C than many other ways. Especially once you

I looked for pretty much the same, and it seems that if you don't use problematic features, you should get closer to C than many other ways. Especially once you activate e.g. LTO compilation or so. Types that can represent bounds can allow further optimization, even possibly reducing the size of struct fields due to the internal-only way of LTO compilation. I would not expect dev time to be longer, except for the initial learning as such/onboarding. My reasons are apparently quite a bit more ambitious than yours though, so it's hard to compare. The cases where I'd go for the hassle that non-standard tooling is, allow large gains from deep static analysis/formal proving of limits due to foregoing conservative, non-adaptive hardware limits. A C-version would look like seL4, including the proofs. I'd try Ada/SPARK for it automating a lot of it away and having specific features to support this "lock elision" use of software verification.