I think this is not a good idea. 1. what kind of security properties do you want to verify. I cannot think of one that could not be checked at runtime when t

I think this is not a good idea. 1. what kind of security properties do you want to verify. I cannot think of one that could not be checked at runtime when the dangerous function is called with actual parameters. 2. turing completeness has nothing to do with security. Before Haskell had IO it was totally safe but still turing complete.