In the last post, we see a definition of developers’ intents that is hopefully not too ambiguous. To recap,

If we abstract programming as a consecutive refinement of state machines: \(S_0 \sqsupseteq S_1 \sqsupseteq \, ... \, \sqsupseteq S_n\) from business requirements (\(S_0\)) all the way down to implementation details (\(S_n\)), an intent is either

  • a decision on how to refine a state machine \(S_i\) (denoted as Type-1 intent), or
  • an assumption to establish \(S_i \sqsupseteq S_{i+1}\) (denoted as Type-2 intent).

This helps us to argue why any software bug can be traced down to violations of Type-2 intents. Taking a step further, This statement has a rather discouraging implication: ensuring absence of bugs requires at least an exhaustive capture of all Type-2 intents from developers and probably intents implied by social norms as well. Unless we are blessed with the superpower on mind reading (…or breakthroughs on brain-machine interfaces…), I tend to be pessimistic about bug-free programs in absolute terms.

Instead, I am wholeheartedly in favor of high-assurance programs that aim to nail down as many intents as possible. Especially, we have a simple intuition for assurance now: the more intents solidified, the more assurance we get, and, for the survival and growth of community-backed projects, the more social coordination1 we can achieve. And this intuition holds for both Type-1 and Type-2 intents. Therefore, I tend to believe that an important goal of a programming language (including its associated toolchain) is to solicit and solidify as many intents from developers as possible.

Capturing intents are tricky

With so many things expressible as intents, there is obviously a hierarchy of expressiveness for different types of intents: some are trivial to declare while others do not even have a proper way of declaration.

  • Implied intents – Intents of this kind do no require explicit declarations as almost everyone knows and agrees to them. Memory safety is a perfect illustration of implied intents: if we malloc a buffer in C, by default we are declaring an intent that no one should overrun it or leaving dangling references to it. Another example is no data races, as we generally do not expect racing accesses to the same memory location by two threads.
  • Intents expressible with a low cognitive effort – Intents of this kind usually require low cognitive burden to express (as writer) and recognize (as reader). Personally, I tend to treat every intent expressible in the type system of the programming language as a low-effort intent. Examples of such intents include the const keyword and the friend declarations in C/C++. Type inference techniques further reduce the cognitive effort.
  • Intents expressible with a high cognitive effort – Intents of this kind are still expressible but requires higher order logical constructs than just the type system, making them harder to read and write. Personally, I like to treat intents captured by formal specifications (in the verification context) as high-effort intents. In the context of the Move language, such intents include invariants over fields within a data structure (e.g., struct S { a: u8 } where a >= 42) or the whole global state (e.g., a normal user can neither mint nor burn coins).
  • Intents not expressible but somewhat documented – This is one reason why code comments and lengthy design documents exist. There is a limitation to everything, including formal verification, not to mention less structured languages. Many times we see lengthy inline comments in the Linux kernel justifying which lock is used to guard gainst racing data accesses. Such intents are simply not expressible within the C type system (but is expressible in Rust, with Mutex<T> for example). and the best a developer can do is to document it thoroughly to warn future code contributors.
  • Intents not even recognized by the developers – People argued that Steve Jobs is one of the the best product designers because he recognized the needs for touch-based UI where users themselves do not even recognize. The Rust language, in particular, its borrow semantics strikes me in exactly this way—I was not even aware that memory safety can be decomposed into such an elegant way and more importantly, when I retrospectively check the C/C++ code I write, most of them are already programmed following these principles.

This hierarchical view leads us to the first principle in evaluating a programming language or a language feature from the intent solicitation perspective. Principle 1: any feature that makes the expression of the same intent easier according to this hierarchy is favorable.

Language features may not be cooperative

Unfortunately, while most language features indeed help to capture more intents, some features just create difficulties and confusions in capturing intents. The worst ones may even encourage developers to shoot themselves in the foot. For example (which is heavily biased by person opinion), type casts in any language is a bad choice as it creates confusion by invalidating intents expressed by possibly other developers. Another example is the re-entrancy feature allowed in the Solidity language which is totally counter-intuitive. As a result, Principle 2: any feature that invalidates other intents or creates counter-intuitive behaviors is unfavorable.

What’s more, human mistakes are everywhere. A developer may accidentally expressed a wrong intent. This is inevitable, but a good language feature should reduce the chances of this happening and catch such mistakes as early as possible. A counterexample is the indirect call features in Solidity. Suppose that the developers’ intent is to call foo but accidentally write call("fooo(string,uint256)") instead. This mistake won’t be spotted by the compiler and not even the VM at runtime (because the fallback function is invoked). So, based on this counterexample, Principle 3: any feature that helps developers identify and correct mistakes early in the development process is favorable.

  1. For more information on social coordination, I highly recommend the talk on Compile-Time Social Coordination by Zac Burns in RustConf 2021. ↩