Formality Considered Harmful - jmp .home

Josh Pollock

I’m a sixth year PhD student at MIT. I work on domain-specific languages for graphic representations.

Follow

@joshmpollock

jopo@mit.edu

@joshpoll

LinkedIn

Custom Social Profile Link

-->

“Formality Considered Harmful”: A Paper I Love

There are some papers that stick in my mind. These are good papers. But there are some papers that when<br>I tell others about them, they stick in their minds as well. These are great papers. “Formality<br>Considered Harmful” by Shipman and<br>Marshall is a great paper.

Let’s dive in!

The Thesis

In this paper, we describe how creators of systems that support intellectual work like design, writing, or organizing and interpreting information are particularly at risk of expecting too great a level of formality from their users. To understand the effects of imposing or requiring formality, we draw on our own experiences designing and using such systems.

Difficulties with Interacting with a Formal System

The authors identify four difficulties of working with formal systems.

Cognitive Overhead

Formalism introduces several types of cognitive overhead:

A user must learn the formal language of the system they are using.

A user must learn how to translate their goals and tasks into this language.

The formal language may introduce incidental complexity – like naming, linking, and labeling.<br>These features are typically necessary to make implicit relationships explicit and precise,<br>especially in written formalisms (as opposed to UIs where direct manipulation can remove the need<br>for some of this complexity.)

Tacit Knowledge

Formalizing a concept requires making tacit knowledge explicit. For example, an English sentence<br>(typically) has a subject and a predicate. Even though I’m pretty familiar with English, this kind<br>of representation is part of my tacit understanding. If a formal system required me to identify the<br>subject and predicate of every sentence, that would be a big stumbling block to my ability to write!

In a software context, a formal system that requires a user to write the type of every variable in a<br>program may require a user to make explicit the tacit data structures they have in their heads.<br>There are a lot of benefits to doing that! But it can also slow a programmer down, especially when<br>they may not have even settled on their types yet.

Enforcing Premature Structure

Knowledge work is messy. Often someone will start with a tacit and informal idea, maybe a vague<br>solution to a problem or fuzzy idea of a system architecture, and they will gradually make this<br>idea more explicit and<br>formal.

This process doesn’t proceed in just one direction either. We often make mistakes and have to<br>backtrack, sometimes literally going back to the drawing board. So formal systems that impose formal<br>structure too early in this process of figuring out an idea are doomed to failure.

Tools like Jupyter notebooks allow users to be messy. They can copy and edit cells to try out<br>alternatives. They can view concrete data to decide what to do next or what experiment to try.

Once you have a better sense of what your experiment looks like, you can start to convert your messy<br>notebook to a Python file or a pipeline. (Something that<br>LineaPy aims to help users to do. I worked for them this<br>summer, in part to further explore these ideas!)

Different People, Different Tasks: Situational Structure

Some formal systems assume there is a single, canonical formalism, but sometimes structure is<br>task-dependent. For example, there are a billion and one todo-list apps, in part because each one<br>chooses to support a different set of tasks by imposing its own unique structure.

Mitigating Problems of Formal Systems

In addition to identifying problems with formal systems, the authors propose several mitigations:

Identifying the Essentials for Task

This boils down to formalizing only what is necessary and nothing more. All type systems, for<br>example, make some tradeoffs on what they choose to formalize and what they don’t. Performing array<br>bounds checking statically, for example, is difficult for both humans and computers. Requiring a<br>human to prove that they never access out-of-bounds memory is a high formal burden.

Evaluating Cost/Benefit Trade-Offs to Select Features

Rather than choosing a specific cutoff point for a formalism, you can present a user with a series<br>of tradeoffs where more formalism = more features. For example, if a user spends time creating<br>styles for their slides in PowerPoint, they can reuse these templates across their presentations.

Gradual Formalization and Restructuring

Related to the above, it can be useful for a system to delay its request for formalism until the<br>system actually needs it. In this way, systems like gradual typing can function with only partially<br>formalized structure. Only when, say, a user wants to do a complicated refactor or document an API<br>might they consider creating that formalism.

This is...