> You can prove that a different construct from a different language can do a different thing because it's a different construct from a different language.
This is the same construct, it's just using python syntax instead of c/c++ syntax. There aren't functional differences between the examples.
[Edit: To elaborate, your initial example translated to python is
while(true):
if x:
break
if y:
break
and there is no way to verify that `x || y` is always true. If you can in fact show that it's always true, you can probably restructure the code to both convey that invariant (use an exhaustive if/else if check) that is better supported by linters and gives you warnings when you miss something.
Writing code in a way that makes it more difficult for both humans and machines to divine your intent should be questioned in review! Perhaps it isn't possible to verify that (but that's also concerning), or perhaps you have some good justification for doing the unusual thing, but then that justification should also go in the code as a comment to give future folks context on why you have a strange and misleading pattern.]
> This is a nice one-liner platitude, but also completely unworkable.
Perhaps, in some cases (yes, we can't always follow NASA's coding standards), but ensuring that most of the time invariants are locally verifiable is possible, that's what typecheckers are, and it's not like Java or Rust are unworkable languages to write code in.
Just because we can't statically encode "this loop halts" as a type, doesn't mean that we shouldn't make that fact clear and verifiable by a human. And "it is incumbent on the person writing the code to justify why it needs an exception from <good practice>" is exactly what code review is for. It's not that hard at all. It's how I review code, and how I expect my code to be reviewed.
This is the same construct, it's just using python syntax instead of c/c++ syntax. There aren't functional differences between the examples.
[Edit: To elaborate, your initial example translated to python is
and there is no way to verify that `x || y` is always true. If you can in fact show that it's always true, you can probably restructure the code to both convey that invariant (use an exhaustive if/else if check) that is better supported by linters and gives you warnings when you miss something.Writing code in a way that makes it more difficult for both humans and machines to divine your intent should be questioned in review! Perhaps it isn't possible to verify that (but that's also concerning), or perhaps you have some good justification for doing the unusual thing, but then that justification should also go in the code as a comment to give future folks context on why you have a strange and misleading pattern.]
> This is a nice one-liner platitude, but also completely unworkable.
Perhaps, in some cases (yes, we can't always follow NASA's coding standards), but ensuring that most of the time invariants are locally verifiable is possible, that's what typecheckers are, and it's not like Java or Rust are unworkable languages to write code in.
Just because we can't statically encode "this loop halts" as a type, doesn't mean that we shouldn't make that fact clear and verifiable by a human. And "it is incumbent on the person writing the code to justify why it needs an exception from <good practice>" is exactly what code review is for. It's not that hard at all. It's how I review code, and how I expect my code to be reviewed.