|
I love this. I think people often underestimate the value of dynamic runtime checks. For certain applications, e.g. many types of scientific/exploratory software, dynamic checks and static checkcs have nearly identical utility. But static checks can get really tricky to work with as a developer. I built a library for doing modular runtime verification in Python (https://github.com/mwshinn/paranoidscientist) and evaluated it for scientific software. In the end, it was pretty effective, but not perfect, and there are some major changes I would make if I were to do this again. One problem was that some of the most important cases to check were important because they were difficult to check. (E.g. some function arguments change the meaning other arguments - this is extremely common in major frameworks like numpy/scipy.) By contrast, the flashiest feature in my package was runtime checking of hyperproperties (i.e. checking properties like monotonicity or concavity that depend on relationships between multiple executions of the function), but this was rarely used in practice. The two most common criticisms I hear about runtime checking are (a) it is just an assert statement under the hood, and (b) the performance hit is unacceptable and the only solution is static checks. Regarding (a), sure, they may reduce to assert statements, but most idioms in programming also "reduce to something under the hood". The question is whether dynamically-checked (refinement) types/predicates are a useful abstraction, and in my experience, yes they are. Regarding (b), you probably don't want to use runtime checks on software intended to be run primarily by people other than the developers. But many classes of problems, software is written as a means of discovery rather than as a tool for someone else to accomplish a particular task. For these problems, runtime checks and static checks are approximately equally useful. Static checks are nice to avoid because they can get you into deep water really quickly, so their scope can be quite limited. Also, people tend to overestimate the performance penalty of dynamic checks. Even complex checks often incur no more than a 10% performance penalty. |
Regarding hyper-properties: I assume they only work on immutable data values, otherwise it would be hard to manage historical objects so that they can be part of any of the predicates.
I'm working on a similar project that you may find interesting: https://odipar.github.io/manikin/. I may want to include hyper-properties in future releases.
edit: found this on hyperproperties: https://lamport.azurewebsites.net/pubs/hyper2.pdf