2 ms·

I can prove, pretty trivially that for i in range(10): Will halt. Slightly less trivially, you can prove that while true: if x:

I can prove, pretty trivially that for i in range(10): Will halt. Slightly less trivially, you can prove that while true: if x: break else: break Will halt. But once the if conditions aren't exhaustive, it becomes difficult, perhaps impossible, to know that you won't end up in a weird unhandled state. Preferring and even insisting upon code that is not only possible, but easy, to reason about is good. Or iow it should be incumbent on you to prove the loop halts, not on the reviewers to prove it doesn't.

arp242 3y ago
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. > it should be incumbent on you to prove the loop halts This is a nice one-liner platitude, but also completely unworkable.
- joshuamorton 3y ago
  > 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.

arp242 3y ago

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. > it should be incumbent on you to prove the loop halts This is a nice one-liner platitude, but also completely unworkable.

joshuamorton 3y ago
> 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.