BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage News Every Truth Can Be Established Where It Applies: an Impossible Thing for Developers

Every Truth Can Be Established Where It Applies: an Impossible Thing for Developers

Bookmarks

Developers can face impossible things in their daily work. Not all preconditions can be checked in code due to the definitional constraints of the programming language.

Kevlin Henney gave a keynote about Six Impossible Things at QCon London 2022 and at QCon Plus May 10-20, 2022.

Programmers tend to assume that all preconditions can be checked. The idea of being able to characterise a piece of code in terms of a precondition and a postcondition dates back to the 1960s and this idea still exists, as Henney explained:

We see this structure in many places, including precondition checking on methods, the given–when–then three-act-structure of BDD, the classic way to organise use cases, and so on.

There are statements within a given system that are true that cannot be shown to be true within that system, Henney argued; this is from Gödel’s incompleteness theorems.

We can have the curious possibility that we can state a precondition in natural language but not in code, Henney mentioned. Sometimes this possibility arises from the definitional constraints of the programming language:

For example, in standard C it is not possible for a function receiving a pointer argument to assert that the pointer is valid. It can assert that the pointer is not null, but not that it is valid. Although I can state the precondition in English, there is no way in standard C to do this. I can only demonstrate correctness by stepping outside the context of that function and seeing how it is used or by using facilities that are outside those of standard C.

InfoQ interviewed Kevlin Henney about impossible things and checking preconditions.

InfoQ: What do you mean by "impossible things"?

Kevlin Henney: There are some things that are impossible according to our understanding of how the universe works.

I had this experience a few years ago with a team when they told me one of the technical challenges they were working on. It was an optimisation and I suggested an approach that would meet the performance requirements. One team member pointed out that my suggestion wouldn’t meet one of their usability requirements. They needed something that met both constraints. After a little discussion I realised what they were asking for was actually not possible. They insisted they had to meet both constraints and not doing so wasn’t an option, no matter how hard it was. I had to clarify that when I said "impossible," I did not mean "very hard"; I genuinely meant that meeting both requirements would only be possible in a universe where the laws of physics concerning time were different to ours. They were not pleased.

As an aside, the paradox was resolved after a little further investigation: it turned out that one of the constraints was not actually a customer requirement, but was an architect’s preference that had been converted into a requirement!

InfoQ: Can you give another example of a precondition that cannot be assumed or tested?

Henney: The Halting Problem tells us that there is no way to write a general algorithm that will determine whether or not an arbitrary piece of code will terminate. This limitation prevents us from enforcing guarantees that otherwise might seem reasonable and easy to state. For example, imagine a method being given a piece of code to call back during its execution. We would like to ensure that the callback returns so our method can complete, but there is no assertion we can write that will ensure any given callback will terminate and ensure that our method will proceed to its own termination.

This article is part of a series on Henney’s Six Impossible Things talk. In an earlier article, he showed that it’s impossible to directly represent infinity or to hold infinite precision on a discrete physical computer, as storage and representations are bounded. Another impossibility is that every question has an answer; developers should increase awareness of unexpected failure modes, advertise the possibility of failure, and use time-outs to recover from waiting for an answer that will never come.

About the Author

Rate this Article

Adoption
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

BT