• First do the obvious thing, actually do the IO:

unsafe def unsafePerformIO [Inhabited a] (io: IO a): a :=  match unsafeIO io with  | Except.ok a    =>  a  | Except.error e => panic! "expected io computation to never fail"

• Then wrap a "safe" operation by the unsafe call.

@[implementedBy unsafePerformIO]def performIO [Inhabited a] (io: IO a): a := Inhabited.default