OK, I think I’m able now to more clearly clarify my discomfort with this proposal and offer a possible enhancement that I believe could make all of this more worthy of the churn it imposes. I can best sum it up as, “Spell out the contract!”. What I mean by this would be to include some meta-language for specifying pre-conditions/post-conditions, that would server 2 purposes:
- Clearly document the contract requirements in a way that can both be consumed by documentation generation in a standard fashion, AND
- has the POTENTIAL to at some point be statically solvable and/or run-time optionally (debug/test only perhaps) enforced
A quick straw-man syntax/idea might be something like:
unsafe ( pre: assert ( ...some predicate DSL... )
post: assert ( ...some predicate DSL.... ) )
fn ( .... ) -> Result
The “some predicate DSL” could be a mini, extensible language that allows expression conditions about the inputs and outputs. It could even allow an “Escape Hatch” like clause that is effectively, “We have no way of expressing this condition in the DSL, but, here is some normal human language that describes the necessary contract”.
That way, we can gradually evolve this DSL to support more and more of the kinds of necessary predicates and eventually work towards linting or otherwise statically analyzing whether or not they have been met.
Again, this is all very, very straw-man at this point and I would have to put significant effort to clarify further (I realize). I’m not an expert on this sort of thing, but, if I had my druthers, this is the direction I’d like to see pursued.
Perhaps this is an entirely orthogonal concern to what you are proposing though.
With this DSL idea, the compiler could parse the DSL predicates, determine (at some future point) if it has the potential to statically solve the predicate, if it CAN solve the predicate, and in the context of the call to the function it is able to verify that the predicate has been met, an “unsafe” block around the call isn’t required. However, if it can’t (yet) verify the predicate, it could spit out an error if no unsafe block is present and display the predicate that it can’t verify. If the predicate includes the “Escape Hatch” predicate, then the compiler obviously can’t verify and will output the the predicate for sure with an error if the unsafe block isn’t present.
If it can’t verify the predicate, but, and unsafe block is present, it would simply output a NOTE/REMINDER (like a WARNING, but, not classified as a warning) that simply reiterates the necessary predicates.
If the call is inside an unsafe block, and the predicates CAN be verified, it could warn about an unnecessary unsafe block.
Why this last? Because, then you will get an error in compiling if you break some code elsewhere that messes up the previously verifiable predicate.
To clarify further, with these predicates there are several possibilities for the compiler to find at the site of a call to an unsafe function (similar argument applies to unsafe returns):
- predicates not specified - unsafe block required/lint on function def advising to add preds
- preds specified, but, not statically solvable (aka compiler support lacking, escape hatch predicate used) - unsafe block required for call
- preds specified, statically solvable (with one of the following possibilities):
- compiler can prove at call-site that predicate not met - COMPILER ERROR
- compiler can prove at call-site that predicate is met - UNSAFE block not required and is NOTE/REMINDERED against (on second thought, prob should be a compiler error as well – I’ll explain below)
- compiler cannot say for sure whether or not the predicate is met - UNSAFE block REQUIRED with output of a NOTE/REMINDER of what predicate(s) are being unsafely relied upon
I think the middle sub-bullet point above is the interesting one. Because the compiler can prove statically that you’ve met the predicate, it should be a compiler error to wrap in unsafe block. Why? Because that way, if you later change the code to break the predicate, you’ll get a new compiler error.