I would love to see refinement types myself. Having tinkered with Ada/SPARK in the past, I am convinced this is great and straightforward way to avoid many bugs.
Once the annotations are in place, a lot can be done to improve program quality, from injecting dynamic tests, to a full formal verification of the entire program.
It is not clear if there is a single best approach, probably a mix of different approaches is best.
As a first step, we’d need a way to attach additional specifications to variables or return values of functions, such as
range
set membership
arbitrary predicates
I don’t think there is currently a way to add attributes to variables, but the user-facing syntax could look like this: @annotation 0 < x < 10 @annotation myPredicate(x) == true
The annotations could also go into docstrings:
"""
N counts the
@annotation n > 0
"""
n::Integer
Based on these annotations, libraries could generate tests, add dynamic checks, or try to statically prove the assertions.
Such checks would not have to be part of the core, different verification tools could use different approaches. As an example, one tool could verify ranges, while another tool could verify physical units.