just document the impure operations and stop forcing the programmer to type extra characters.
To me, the main draw looks to be the invariants that you can supply within functions, but this isn't a new concept outside of it being a dedicated keyword. Otherwise this looks like rust without all of the functionality