Way to disable side effects?

Stream: lean4

[Alissa Tung]

I am curious about is there any way to restrict or disable side effects in user code. For example, disable executing programs, performing file IO and network IO and something else.

Since one can show from an IO do, performing any IO action in TacticM, and so on...

[Henrik Böving]

Not from Lean directly but operating systems have adapted mechanisms for this by now. You can for example use bubble wrap or the syscall APIs like seccomp directly.