Reconsider omission of precondition from `popLast`

[katzdm]

While concluding the study of the popLast example, the Contracts chapter recommends removing the explicitly documented precondition. I think this is worth reconsidering, as there might be any of several behaviors that a caller could expect from empty.popLast() - Will it throw? Terminate? March off into UB? Return a null or default value? Some of these behaviors won't be possible in some languages, but an explicit precondition tells me: "This is an assumption that the caller is responsible for fulfilling; don't count on any particular behavior if it's not met." Omitting the precondition makes the function feel under-documented, and leaves the width/narrowness of the contract something that must be interpreted/inferred (which is probably a higher cognitive load than reading a few extra words).

An argument could be made that a caller should not "reasonably expect" some of the above behaviors if they aren't documented. I think that perspective is "technically correct", but not necessarily productive: Explicitly documenting the precondition better guards against "unreasonable" (i.e., tired, under-a-deadline, quick-reading, etc) callers.

[camio]

Explicitly documenting the precondition better guards against "unreasonable" (i.e., tired, under-a-deadline, quick-reading, etc) callers.

I tend to agree with this, especially if calling outside the contract can result in undefined behavior.

[dabrahams]

• it can't throw because Swift makes you label throwing functions with throws. You can see that from the signature.
• It can't march off into UB because Swift is a safe-by-default language and popLast isn't labeled unsafe (putting unsafe in the name is how it's done in Swift).
• It can terminate. It can also do anything else unspecified.

You don't document what happens in the case of precondition violation because then it's no longer a precondition. For example, if we were to say the function will terminate, we can no longer say, without exception, that popping from an empty DynamicArray is a bug. It would be correct to use it to intentionally terminate the program. Diluting the power of preconditions in this way is a bad idea.

[katzdm]

That makes sense - Rather than suggesting that you document the behavior in the presence of a failed precondition though, I'm instead suggesting that it seems valuable (in this example) to keep the explicitly documented precondition.

[dabrahams]

What makes this one example special? For an unsafe operation, I would support documenting all preconditions explicitly. This is not that.

[katzdm]

My impression is that the intended audience for "Better Code" is broader than just Swift developers - I imagine, for instance, that you'd like for it to be useful to C and C++ developers. If so, perhaps this point:

For an unsafe operation, I would support documenting all preconditions explicitly. This is not that.

could be stated more explicitly. The chapter currently justifies the removal of the precondition with the following:

Whether or not to omit an implied precondition may be a slightly different judgement from the others, because it's information every client needs in order to use the function correctly. We recommend omitting explicit documentation of any implied precondition unless it's quite subtle.

But it sounds like another part of the calculus is whether the operation is safe. What do you think of the following?

Whether or not to omit an implied precondition may be a slightly different judgement from the others, because it's information every client needs in order to use the function correctly. Preconditions whose failure can cause the program's behavior to be undefined should always be stated explicitly, so more verbose documentation may be necessary when using a language with unsafe defaults (like C or C++). When using a language like Swift, we recommend omitting explicit documentation of any implied precondition unless it's either quite subtle or it applies to an unsafe function .

Do you think something along those lines would be worth calling out?

[dabrahams]

Yes, as a consequence of you filing this issue (thanks!) we're going to cover that; see #28. There's enough about unsafe operations to warrant its own subsection, so I think we're not going to put it in that paragraph.

Note, FWIW, there's no unsafe keyword in Swift.

[katzdm]

Sounds great, thanks for being receptive to the suggestion!

there's no unsafe keyword in Swift.

Next time, I'll ensure that my research consists of more than "a single google search" (even if that's just, "a single google search and clicking on one of the links") 🤣

[dabrahams]

@katzdm Closing; if you feel there's something unhandled feel free to reopen.