It would be interesting to also "weave" in test cases. The workface of logic statements is exactly where bugs are introduced.
Especially around temporal events, and that goes to formal models (and even more bugs).
Typically, if there is a rule around height, there would be at least three tests¹: one taller, one equal to, and one shorter. (Without types or something, then also negative, null, and max/min boundary inputs too.)
So you could have tests based on timelines, like
Given a regulation is passed in 3 months
And parties are prevented from exercising B
But "17 tons" of waste are dumped anyway
And ...
When ...
Then ...
Having a model checker integrated would be a boon. Maybe we could have DevOps-like pipelines in formally-verified legislature (or at least the encoding of language to code).
Many laws are written with a lot of double meaning (recent eu regulations on allowing or not allowing russian cars is a good example).
Though, it could be a good idea to find all the possible double meanings or vague definition when trying to "digitise" the laws into the programming language.
Right, some laws are just ftp-dragged & dropped to prod, understanding that it doesn't compile yet. But if legislator managed to express the _intention_ the courts will over time add and make all test cases pass.
I'm sure the mentality of a PHP developer running a successful but insane legacy site is a better model for this than a perfect OCAML project :)
This is great. I often look at unit tests to understand how to use legacy code. Seeing a law come with concrete examples that are part of the legal text, would allow us to test if a rule is logically consistent, and test our understanding as well. Sort of how you want to convince your reviewer that your code works by proving it with a unit/integration/e2e test.
Especially around temporal events, and that goes to formal models (and even more bugs).
Typically, if there is a rule around height, there would be at least three tests¹: one taller, one equal to, and one shorter. (Without types or something, then also negative, null, and max/min boundary inputs too.)
So you could have tests based on timelines, like
Having a model checker integrated would be a boon. Maybe we could have DevOps-like pipelines in formally-verified legislature (or at least the encoding of language to code).¹ https://en.m.wikipedia.org/wiki/Equivalence_partitioning