> 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?