[Darmani]

> just to point out that his notation just begs the question of what do(X) means,

It's very formally specified. The key object of study in Pearl-style causal inference is a structural causal model. A structural causal model is composed as equations like the following:

Y = f(X, Z, U)

Here, X and Z are observed inputs, other random variables in your system. U is unobserved. In other words, "Y is computed by a deterministic function which takes an unknown random input."

Then, P(Y = 1 | do(X=1, Z=2)) is defined as P(f(1,2, U) = 1).