This isn't just a notice to programmers that a subprogram may be "conceptually pure", whatever that actually means. It should be formally verified because there are numerous optimizations and various features that can be implemented in a function-level environment.
One of the most obvious and easy to explain is compile-time expression evaluation. This is only possible in a function-level environment, and formally and statically verifying this directive would allow for this possibility.
Another is proving thread safety. A function-level subprogram is always safe to use in a concurrent environment without locking.
Ada does:
or
This doesn't do anything. No seriously.
It should be:
Actually statically verified
Rationale:
This isn't just a notice to programmers that a subprogram may be "conceptually pure", whatever that actually means. It should be formally verified because there are numerous optimizations and various features that can be implemented in a function-level environment.
One of the most obvious and easy to explain is compile-time expression evaluation. This is only possible in a function-level environment, and formally and statically verifying this directive would allow for this possibility.
Another is proving thread safety. A function-level subprogram is always safe to use in a concurrent environment without locking.