I've been writing [libsodium](https://doc.libsodium.org/) bindings in Lean4 and have ended up using `native_decide` quite liberally, mostly as a convenience. Can any Lean devs provide a more thorough interrogation of this? Should I go back and try to scrub its usage out of my library? Logically it seems consistent with what I'm trying to do with Lean4's FFI (i.e. you really do need to explicitly trust the Lean kernel since I'm adding nontrivial computation using a foreign cryptography library) but I'm curious if this isn't necessary and whether Lean devs would push back on its use.
Comments
I've been writing [libsodium](https://doc.libsodium.org/) bindings in Lean4 and have ended up using `native_decide` quite liberally, mostly as a convenience. Can any Lean devs provide a more thorough interrogation of this? Should I go back and try to scrub its usage out of my library? Logically it seems consistent with what I'm trying to do with Lean4's FFI (i.e. you really do need to explicitly trust the Lean kernel since I'm adding nontrivial computation using a foreign cryptography library) but I'm curious if this isn't necessary and whether Lean devs would push back on its use.