3 ms·

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

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). ¹ https://en.m.wikipedia.org/wiki/Equivalence_partitioning https://en.m.wikipedia.org/wiki/Equivalence_partitioning

natn 3y ago
imagine... TTD applied to laws. Or take it a step further, write a test suite and automatically generate a range of possible laws that satisfy the tests.
octacat 3y ago
It will not compile (sarcasm). 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.
- ragulpr 3y ago
  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 :)
az09mugen 3y ago
That would be nice also to have unit tests
justusw 3y ago
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. End to end tests for legal frameworks?

natn 3y ago

imagine... TTD applied to laws. Or take it a step further, write a test suite and automatically generate a range of possible laws that satisfy the tests.

octacat 3y ago

It will not compile (sarcasm). 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.

ragulpr 3y ago
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 :)

az09mugen 3y ago

That would be nice also to have unit tests

justusw 3y ago

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. End to end tests for legal frameworks?