Missing operators about bedrock2 HOT 1 OPEN

I don't see any real reasons to prefer notations to new bopnames as long as the operation is generally useful. If giving semantics directly would result in nicer proof obligations, I'd say let's prefer adding bopnames.

I think you could do "! x" := (x == 0) if you wanted, though?

&& and ||: as primitives, added to bopname, or maybe using a ternary if?

I think we should only add them if we are going to match the semantics of C and its predecessors (and at that point we could indeed add conditional expressions as well). In particular 0 && *0 should be a safe expression. We could totally do this (heck, with the confidence we now have about postcondition-style semantics I'd feel fine even going to everything-is-an-expression land), but my hunch is that it's not the most impactful thing to work on right now.

from bedrock2.