[Ygg2]

If you sacrifice memory safety for correctness, that just means it's not correct. If safety is crucial, it must be safe under all inputs, and if there are data races.

It's a bit like saying, "Yeah, our system is safe, but if there are two threads racing or use after free somewhere, then all bets are off."

[n42]

you do not sacrifice memory safety. you sacrifice a compiler ensuring that code is memory safe by it enforcing one quite opinionated approach to it: RAII and lifetime analysis.

you seem to think there is one path to memory safety. there is not. unsurprisingly, some programmers may need different tools when working with a different set of requirements.

[Ygg2]

If you're using Zig to write correct by design code you do.

Or at least you have to add memory safety as another extra step on your road to correct by design.

I'm aware of paths to memory safety, but they boil down to: pervasive GC, annoying compiler, and praying you got it right.

If you write your proof in GC language than translate it to C, that's just a mix of pervasive GC and praying.