Such an interesting project. A non-trivial amount of my consulting work has been in translating statutory requirements into system architecture features as they relate to requirements for privacy and security, often with cryptography. Along the way, you see how laws are not meant to run on machines or be subject to mere logic, and they are not abstract state machines that yield "legal," under the right conditions.
I'm not a lawyer at all - but I am a technologist who builds systems that people and institutions punt thorny legal and ethical decisions to, and they use the tech as a black box of risk, where they hope they can't be held accountable to understand the conseqeunces of the implementation.
The point of most cryptography and security features is to use math to represent and symbolically transfer liability and risk between transaction counterparties, where, law also determines a balance or flow of symbolic liability and risk between parties.
The idea of modelling laws as concrete logic is appealing, but it presumes the quality of a law is if it is resistant to individual interests, judgment and interpretation. To me, that sets up a conflict where the best possible law is either, one that obviates the need for a judge or litigation - vs. - being the most refined and featureful tool for people (and judges) align things like morals, principles, ethics, and interests.
The author's example of that inconsistent common law definition where you didn't actually have to live together in a relationship is arguably an artifact of Canadian charter and British common law where individuals do not have inalienable rights because ultimate and total authority rests with the crown. It doesn't have to be logical or consistent, but this is just my layman observation.
If the written law is illogical, a judge interprets it, and gives it back to the government to refine, and the government often just ignores it until there is a new patron to appease by changing it, or if it doesn't give them the result they want, they just update the regulations of the law without a requirement for debate. Automating legal analysis in Canada seems like more of a way to find arbitrages and loops than to provide any general efficiency or benefit.
Is that what this formal methods project is doing, or do they think people will accept being subject to automated legal decisions?
I'm not a lawyer at all - but I am a technologist who builds systems that people and institutions punt thorny legal and ethical decisions to, and they use the tech as a black box of risk, where they hope they can't be held accountable to understand the conseqeunces of the implementation.
The point of most cryptography and security features is to use math to represent and symbolically transfer liability and risk between transaction counterparties, where, law also determines a balance or flow of symbolic liability and risk between parties.
The idea of modelling laws as concrete logic is appealing, but it presumes the quality of a law is if it is resistant to individual interests, judgment and interpretation. To me, that sets up a conflict where the best possible law is either, one that obviates the need for a judge or litigation - vs. - being the most refined and featureful tool for people (and judges) align things like morals, principles, ethics, and interests.
The author's example of that inconsistent common law definition where you didn't actually have to live together in a relationship is arguably an artifact of Canadian charter and British common law where individuals do not have inalienable rights because ultimate and total authority rests with the crown. It doesn't have to be logical or consistent, but this is just my layman observation.
If the written law is illogical, a judge interprets it, and gives it back to the government to refine, and the government often just ignores it until there is a new patron to appease by changing it, or if it doesn't give them the result they want, they just update the regulations of the law without a requirement for debate. Automating legal analysis in Canada seems like more of a way to find arbitrages and loops than to provide any general efficiency or benefit.
Is that what this formal methods project is doing, or do they think people will accept being subject to automated legal decisions?