that is correct. however, zz does enforce api contracts which can be arbitrary expressions within the QF_UFVB theory. for example check out the err::checked()

that is correct. however, zz does enforce api contracts which can be arbitrary expressions within the QF_UFVB theory. for example check out the err::checked() theory which enforces that a function call must be followed by err::check. similarly, i expect a community will come up with other standard contracts such as must_not_copy() for secret values that may not be copied.