What does it really mean to formalise something? And what kinds of things should we be interested in formalising?

Law is an obvious example of a domain with rules that are almost formal.
Law has rules that can be described using deontic and default logic.^[1]

When we talk about formalising a domain like law, here, we're talking about formalising something with rules. But, in most real-world domains, there's more going on than just rules.

While it makes a lot of sense to formalise law as a set of rules in formal logic, for domains like software engineering, chip design, mechanical engineering, the structure is more readily formalised as a system. Something with input, output behaviour, an internal state. And often, with an interface to the environment, making the system an open system.

Let's, first of all, try to understand what really is a domain in its entirety? If it's not just a set of rules, what is it? And if we're trying to formalise a domain mathematically, how do we know when we're finished?

Maths -- specifically, proving mathematical statements, is a domain that, when looked at from the Lean lens, is about writing proofs as programs where types are theorems.^[2]

Law -- a domain that is formalisable in default logic. Simple legal arguments can be seen as closed, static programs (in the same way as mathematical proofs). But complex, real-world legal arguments often require input from an external environment (such as a judge in court).

Chip design -- a domain where we’re concerned with open, dynamical systems (chips) which interact with their environment and usually change an internal state.

Mechanical Engineering -- a domain where we have open, dynamical systems (physical designs), usually along with a set of design specifications, and rules defined by industry standards

It's starting to become clearer how we might categorise our domains. Specifically, each domain is made up of systems with a combination of properties (open/closed, static/dynamic, deterministic/stochastic, terminating/non-terminating etc.):

open/closed, static/dynamic, deterministic/stochastic, discrete / continuous, Markov / history-dependent, time-invariant / time-varying, linear / non-linear, stable / unstable, reversible / irreversible, autonomous / non-autonomous, monolithic / compositional, finite / infinite state, terminating / non-terminating (aka reactive)

Each of these properties describe a broad set of systems. The properties can each be defined mathematically and formalised in Lean. Unfortunately, Lean is also missing a lot of machinery. For example, we would really want co-inductive types for defining non-terminating systems. Working with probabilistic systems is also hard.

The domains most readily available to formalise in Lean are those that contain closed, static, deterministic systems. E.g. algorithms, mathematical proofs or simple legal arguments.

So, going back to the original question, what does it mean to formalise a domain?

It means to describe a collection of sub-systems, how they interact with each other and with their environment. Rules are just the case where a system is closed.

References