> You lose soundness, but we don't have sound guarantees for functional correctness, anyway
This sounds like "we can't guarantee the most important thing, so it's unclear whether it's useful to guarantee this other thing," but that's a bizarre statement, so am I misinterpreting?
It means that there's a complex tradeoff between making sound guarantees and providing correctness in other ways, a tradeoff that all languages make anyway, each finding its own preferred sweet spot, and that we don't know if, say, Rust's sweet spot yields better correctness than Zig's.
