What does it mean to "formalise a domain"?

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.

So, maybe when we're talking about a domain, here, we're talking about 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.

The way we can verify an open system is through assume-guarantee contracts. These generalise the idea of pre-condition/post-conditions we use to verify programs: we have an assumption (model) of the environment and, given this assumption, a guarantee on the behaviour of the system.

But let's not get too bogged down in the technicalities. First of all, let's try to understand, really, this idea of a domain and what the full space of domains looks like.
I would also like to look at how each domain may be formalised in Lean.

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.

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, observable / partially-observable (internal state), controllable / uncontrollable, 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 still missing a lot of machinery, for example, we would really want co-inductive types for defining non-terminating systems.

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 deciding what kind of system the domain is made of, what that system assumes about its environment, and what outputs it can guarantee, given those assumptions. Rules are then just the case where the environment has no effect on the system.