Monads in Haskell serve two purposes.

A monad that is defined *within* Haskell is really a *simulation* of some computational effect in terms of pure (side-effect free) computation. After all, Haskell is a pure language.

The second use of monads in Haskell, as well as in programming language semantics, and many other languages, is to model *external* or *primitive* computational effects. Such effects cannot be defined within the language itself. They necessarily come from some external environment (hardware, operating system, virtual machine).

In Haskell the monad that gives access to external effects is `IO`. This is why the main program has the type `IO ()` – so that it can actually interact with the external world through computational effects.

The ML-family of languages differ from Haskell because they do not separate so cleanly the pure & effectful computations. In such "impure" languages, *all* computations happen in a single `IO`-style monad that gives access to all external effects (I/O, mutable memory, exceptions) all the time. And the fact that this is the case is *not* recorded in types. Thus, an ML computation of type `int` would really be something like `IO Int` in Haskell.

Of course, the programmer is free to define their own monads in ML to simulate various computational effects, just like in Haskell, but this is a bit irrelevant here.

You ask how the effects are specified in the formal semantics. There are several ways of doing it (transition semantics, algebraic semantics, abstract interpretation), and I am not sure that describing them here would serve a purpose. Please ask for further references if you'd like to know the details.

The important thing to understand is the *relationship* between the formal semantics, which is the mathematical model of computational effects, and the actual implementation by the language compiler, which converts source code to machine code that triggers computational effects by using the available hardware, possibly via some system calls. We want the mathematical model and the compiled code to match, i.e., the compiler should be *correct* with respect to the formal semantics.