>Can the compiler check that a function is pure besides its assigned side effects?

The compiler can't. It is up to the programmer to make sure that a database effect doesn't, say for sake of example, write out to a file also.

So in the end this is just a novel new way to organise code.

If the database effect wrote to a file it'd require the `IO` effect and code using it would need that effect as well. A compiler can generally show a function to be free of most side effects if it uses no effects. The exceptions to this are things like divergence. As long as the language is Turing complete you can't prove it won't loop forever of course. Another exception could be extern functions which the compiler can't verify the correctness of the type signature. Different languages handle these differently but if users are allowed to write any (and the language doesn't force them to have an IO effect) then they can be a source of unsafety. Languages like Koka and Effekt are considered pure though and enforce this through their effect systems.

so there is side effects propagation and inference I guess.

That has to require some help from the tooling/IDE.