Just like computer programs, mistakes happen with legal languages, and when they do, they are typically have unintended consequences.
(edited for a couple of missing words in the last sentence)
Just like computer programs, mistakes happen with legal languages, and when they do, they are typically have unintended consequences.
(edited for a couple of missing words in the last sentence)
I think the biggest difference they face is that the interpreter is another reasoning human, and not just a functional part of the machine.
There are tons of ambiguities and other problems in issued patents!
When I get the time, I intend to rewrite a significant amount of the code in an object-oriented style. (Basically, making a class for a patent claim and having a ton of methods for that.) The code right now is a mostly untested mess that seems to produce decent results but is not pleasant to work with.
I thought it was the most fascinating talk in the conference.
https://www.youtube.com/watch?v=EshxZVMURt4
https://popl18.sigplan.org/details/POPL-2018-papers/3/Formal...
The city is Los Angeles, though the content doesn't seem to match precisely what was mentioned.
I found this via a Google search for `conference convert legal phrases into code "theorem" bug`, which returned the following paper:
https://hal.inria.fr/hal-03159939v2/document
I then checked the citations of that paper for anything matching.
Oh wait, everyone was a nerdy person!
More seriously, this means you also have to accurately encode all the things the laws refer to, even when those things are vague judgement calls. It's easy to say "you can only have a noncompete agreement if it doesn't make it unreasonably difficult to find another job in the same industry", but hard to express "unreasonably difficult" or "same industry" with the kind of precision we expect from code. A sufficiently evil company would just pay a lawyer for a few days to find a loophole in whatever definitions you can think of.
There's a reason the primary use of this is cryptocurrency conversion - it's a lot easier to enumerate all the failure modes in "give me n of A and I will give you m of B".
Don't need to encode it in some sort of machine code. Just need a git repo with the law so we can submit a PR to the CA assembly and get this fixed.
[0] https://www.cs.virginia.edu/~cr4bd/4630/S2021/
[1] https://exercism.org/tracks/x86-64-assembly
Update: Exercism seems to only be an "exercises" platform and doesn't actually have any teaching materials of its own?
While Leibniz is widely known for his mathematics and philosophy, one of his lesser known ideas was the relation between law and computation.
There is a small research community around it today. Look up Computational Law and Computational Contracts if you are interested.