[HN Gopher] Utterly Unpersuasive: Formal Methods and Law (2019)
___________________________________________________________________
Utterly Unpersuasive: Formal Methods and Law (2019)
Author : zeristor
Score : 53 points
Date : 2022-04-21 09:57 UTC (2 days ago)
(HTM) web link (roundtablelaw.medium.com)
(TXT) w3m dump (roundtablelaw.medium.com)
| errantmind wrote:
| For most applications, developing quickly is more valuable than
| correctness. That is why formal methods will likely never have
| widespread adoption.
|
| As for law, a judge always makes the final decision and they are
| not a formal method. It doesn't matter how tightly the law is
| worded if a judge is in the loop evaluating intangibles like
| intent.
| locusofself wrote:
| As someone who hacks on code but doesn't have a true computer
| science or math background, I have a hard time even wrapping my
| head around what the hell "formal methods" are. How can you write
| proofs that a whole piece of software works? Especially since
| software is often compromised of tons of different libraries and
| frameworks etc.
|
| I could understand proving a certain piece, like a specific
| algorithm, but how are formal methods better than unit tests?
|
| I think my brain is just too small to understand. It feels to me,
| as a relative layman, like pablum.
| andrewflnr wrote:
| You correctly understand the difficulty. AFAICT formal methods
| only really work in relatively small, self-contained scenarios.
| You wouldn't want to attempt a formal proof of a Python web
| app. The seL4 microkernel is one of the biggest verified
| projects I know of. Maybe reading about that would give you an
| idea of how things get put together in the field.
| dwohnitmok wrote:
| Formal methods in a nutshell are using code to statically
| analyze and prove things about code. The reason this has value
| despite sounding circular is that often times the code we use
| to write the statements we wish to prove is easier to
| understand than the code we are proving.
|
| It is fundamentally the reason why tests are useful, despite
| also being code. Even though tests themselves may contain bugs,
| they are still useful because they are simpler and easier to
| understand than the code being tested.
|
| > how are formal methods better than unit tests?
|
| Strictly speaking, unit tests are a kind of formal method. They
| are after all code being used to test code. Other formal
| methods tend to try to concern themselves with universal
| statements rather than one-off examples as unit tests do. E.g.
| proving that a program will never crash no matter what input is
| given to it (whereas a unit test would prove that a program
| will not crash for a single given input).
| motohagiography wrote:
| 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?
| Spivakov wrote:
| "The point of most cryptography and security features is to use
| math to represent and symbolically transfer liability and risk
| between transaction counterparties"
|
| What is the liability here? For example, the company holds
| different level of liability in a data breach, depending on
| whether they implement the security correctly - is that what
| you mean?
| motohagiography wrote:
| Example would be whose keys encrypt and decrypt data realizes
| legal things like custody and control and the associated
| responsibilities.
|
| One area that has recently changed is "de-identification,"
| which used to essentially be a cryptographic problem, but now
| it's a legal definition where you assert a policy about the
| data encoded in a way and subject to a risk assessment to
| make that assertion, and then the de-identified data
| (PII/PHI) now comes with obligations.
|
| Another example was chip/pin payment cards several years ago,
| where they transferred liability to the merchant for fraud
| and chargebacks, where previously, magstrip meant the
| liability for chargebacks largely stayed with the issuer.
|
| If an online banking account gets hacked, banks have less
| liability than they did previously - as even though you must
| assert it was they who were robbed and not you, and they
| still owe you the money you deposited with them, enhanced
| authN/MFA has allowed them to imply it's somehow your fault
| that someone stole the money you trusted them to hold for
| you.
|
| The security of each tech divides the liability between the
| parties in these cases.
| smitty1e wrote:
| "Complexity is a subsidy."--Jonah Goldberg
|
| If they screwed up and put me in charge, I would force this sort
| of analysis on the tax code.
|
| Watching the bureaucracy go to war against the idea of coherent
| public law would be instructive.
| genneth wrote:
| This is doubly unpersuasive in any common law jurisdiction. The
| whole point of such a system is that the idea that the correct
| outcomes are easier to arrive at in the specific than the
| general, and that the codification happens after precedents.
|
| Even in civil law systems the fact is that case law is a
| coexistent partner to the interpretation of texts.
|
| The fact this guy is _learning_ law should actually be a cause of
| not taking this very seriously. I would be more interested by a
| practitioner making the case. (I am not!) In fact, this applies
| strongly to the case he gives: I would bet no judge in Canada
| (outside of Quebec, maybe?) would take his argument seriously.
| The way he has approached this question honest smacks of ivory
| tower academia.
|
| If you made be steelman the argument, it should be that the usual
| methods predate the era of formal methods, and that the overall
| system could be made better. Then one would have to explain
| better in an operationally important way for practitioners and
| workers in the system, usually by some convincing argument about
| time saved. Remember that arguments over definitions is a very
| small part of the time taken in the job!
| mbrodersen wrote:
| A great read. I had the same experience proving (toy) software
| correct: the act of formally specifying what you want to prove
| and proving it makes you understand the problem and the solution
| much better. It's like your brain gains super powers.
| User23 wrote:
| Even an informal process like TDD is a huge improvement in this
| space. You can't write tests first without an at least implicit
| specification.
|
| It is really wonderful though when the algorithm just falls out
| of the specification. Dijkstra's derivation of smoothsort[1] is
| a nice example.
|
| [1]
| https://www.cs.utexas.edu/users/EWD/transcriptions/EWD07xx/E...
| nonrandomstring wrote:
| Not too long ago in computing history there was a fascinating
| confluence of hackers and lawyers who came together to co-examine
| their respective formalisms. It was called Groklaw, run by an
| energetic blogger named Pamela Jones [1]. For many years it
| served to translate law into code and code into law, as well as
| being an experiment in the "many-eyes" idea of picking through
| legal prose in a participatory, public way.
|
| Powerful interests did not like this. Jones eventually tired of
| defending what can only be described as a first generation
| optimist's understanding of the Internet as a tool for social
| good.
|
| [1] possibly a nom de plume of several law and technology
| researchers
| whatshisface wrote:
| Powerful interests?
| formerkrogemp wrote:
| It could sound like a conspiracy theory or it could be as
| simple as the copyright holder of a state's legal code
| abusing DMCA. Who knows?
| nonrandomstring wrote:
| The website [1] is actually still up, so you can read and
| make your own mind up. Alternatively there's a quite
| comprehensive Wikipedia entry [2]. What do you think
| happened?
|
| [1] http://groklaw.net/
|
| [2] https://en.wikipedia.org/wiki/Groklaw
| lauv0x wrote:
| quantified wrote:
| One purpose of hiring a lawyer is to find loopholes. One business
| model for lawyers is selling the exploitation of loopholes.
| Sounds like formal methods can be very valuable in legal
| training.
| lobstey wrote:
| But unlike computer security, laws are not determined by
| hardware that never complain about exploitation. Law is
| operated by humans, and people may reject exploration by
| arguing the contract differently. Lawyers are trained to
| dispute humans rather than rules.
| oh_sigh wrote:
| A human just sounds like a buggy, inconsistent compiler in
| this case.
| bobthechef wrote:
| A Procrustean view.
|
| The law isn't perfect, and in that sense, it is like
| software in that it is constantly changing in anger. With
| the law, however, you're also in the situation of having
| many different interpreters. Given that the law is
| imperfect and requires refinement and adaptation in anger,
| given the imperfect knowledge of law givers, it is expected
| that there would be multiple interpretations.
|
| Law does not determine justice by virtue of its
| codification. Morality does. Law is just the determination
| of general moral principles. A ruled-based system blindly
| followed by a machine would be a disaster outside very
| narrow, niche applications.
___________________________________________________________________
(page generated 2022-04-23 23:01 UTC)