[lmi] Are NAND assertions difficult to understand?

[Greg Chicares]

An insurance policy comes into being when it is "issued";
that occurs on its "issue date".

Some events can occur only on the issue date, while others
can occur only after the issue date, so it's important to
know whether the policy was issued today.

A policy has a "duration", which is the number of full
years elapsed since the issue date.

For example:

  issue date  date today  duration?  issued today?
  ----------  ----------  ---------  -------------
  2021-03-05  2021-03-05      0           yes
  2021-03-05  2021-03-07      0            no
  2021-03-05  2028-03-05      7            no

One subsystem passes
  struct {int duration; bool issued_today;} args = {/*values*/};
to another, which must validate the passed-in object by asserting
the following invariants--expressed as simply as I can imagine:
  args.issued_today → 0 == args.duration
  0 != args.duration → !args.issued_today
or in natural language:
  if the policy was issued today, its duration must be zero
  if duration != 0, the policy cannot have been issued today
What's the clearest way to express that in code?

Is the following "NAND" assertion too obscure?

  assert(!(args.issued_today && 0 != args.duration)

Is the following equivalent more understandable?

  assert(!args.issued_today || 0 == args.duration);

I'm torn between them, because the NAND formulation:
  args.issued_today | 0 != args.duration  // Sheffer stroke
  args.issued_today ⍲ 0 != args.duration  // APL
seems obvious to me, and terseness does favor clarity.
However,
  https://ilk.uvt.nl/~pvogt/publications/Scriptie-MaartenVanWijk.pdf
  [only a few logical connectives, e.g. {∧,∨,¬}] "are expressed
  using single-morpheme lexicalisations in natural language" ...
  "no known natural language has lexicalized '|'"
Yet the lack of a single word for '|' doesn't mean we can't
express this in natural language by using more morphemes:

  The propositions
    - the policy was issued today
    - it's in a renewal year (duration is not zero)
  are mutually exclusive.

OTOH, the OR formulation:

  ¬args.issued_today ∨ 0 == args.duration

may seem simpler, but if I translate it to natural
language:

  Either the policy wasn't issued today,
  or it's in its first year (duration is zero).

it seems artificial--I want to turn it into the
NAND form to make it comprehensible.

I could take the way we'd explain it to non-logicians:
  args.issued_today → 0 == args.duration
  0 != args.duration → !args.issued_today
and translate that directly:
  if(args.issued_today)
    assert(0 == args.duration);
  if(0 != args.duration)
    assert(!args.issued_today);
That seems easier to comprehend; but do conditional
assertions seem uncomfortably weird in C or C++?
Would a programmer wonder whether an error underlies
this unusual construct, and mentally try to unify
them in order to understand the meaning?

I tried combining those assertions into one statement,
but found it difficult to do correctly:

  assert
    (  ( args.issued_today && 0 == args.duration)
    || (0 != args.duration && !args.issued_today)
    ); // WRONG

That's wrong: it fires in the valid case
  args.issued_today = false;
  args.duration = 0;
It could be corrected, but that would make it
really hard to understand.

The problem vanishes if we traffic in dates or JDNs,
but that cure is worse than the disease because it
requires a calendar class, and forces us to use
concrete dates where we'd rather use abstractions.