People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.
At least the metamath verifiers will not bend over backwards and come up with absurd inconsistent counterarguments.
It's the most humiliating thing for citizens when the legal cadre of a nation pretends in the national journal that everybody falls for its lies... openly mocking the concept of truth itself with absurdism.
Formalisation can't save you from determining what is and isn't a document. The judges main task is formalising reality and lawd, the rest of the inference is typically easy.
>Formalisation can't save you from determining what is and isn't a document.
I'm not sure what this sentence even means, of course the democracy should have define those.
its up to the electorate to democratically define what is a document, to define classifications of types of documents, and which ones are administrative.
> The judges main task is formalising reality and lawd, the rest of the inference is typically easy.
Except the judge is plainly ignoring valid derivations, and as a verifier making silly "proofs" up (civil law, not common law) in full-frontal-nudity on behalf of one party.
The problem is not the concept of law, nor the concept of democracy, nor the concept of formalization: the problem is how do we defend against and formalize a response to corrupt verifiers in the legal system?
Those who understand technology to verify arguments already exists can only come to the conclusion we'd be better of with formal verifiers in legal systems.
> Those who understand technology to verify arguments already exists can only come to the conclusion we'd be better of with formal verifiers in legal systems.
Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.
No formal verifier can account for definitions that need to expand as the scope of human endeavor expands. No formal verifier can determine mens rea. No formal verifier can determine if something is obscene. No formal verifier can determine someone's mental competence. No formal verifier can cover all mitigating factors. No formal verifier can apply mercy where mercy is needed.
> Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.
Not the vagueries of human existence, only vagueries of law specified in natural language.
> No formal verifier can account for definitions that need to expand as the scope of human endeavor expands.
No formal verifier is expected to account for definitions, the democracy shapes the law, and the law would first need to be rewritten as definitional axioms in the database of axioms, theorems & proofs. The verifier is just a minimalistic algorithm performing substitution maps on sequences of tokens. This is intentionally minimalistic to minimize the error / attack surface on the verifier itself.
(Currently only error hardening has happened for metamath verifiers, so obviously we would want formal proofs of the absence of 0-days in the verifier)
> No formal verifier can determine mens rea.
It's up to the democratic population while formalizing, to either formally define intent (which presumably goes nowhere), or to pragmatically accept that in the absence of external traces of intent the only thing society can do is define action-reaction patterns, not intention-reaction patterns, but again, that's not the formal verifier, but the database of axioms, definitions (and theorems and proof)
> No formal verifier can determine if something is obscene.
The same, if democracy by referring to a concept of "obscene" chooses to place itself in the position of needing
to first define "obscene" in the database of axioms and definitions. But no formal verifier needs to determine this, the verifier just checks a proof in a due process fashion.
> No formal verifier can determine someone's mental competence.
The formal (not natural langue) law could specify how to assess mental competence in a secure non-malleable way (if the democracy decides it needs that). I'm not a dictator, it's not up to me to propose the exact definitions. The formal verifier is not the place to handle these issues, those should reside in the database of axioms and definitions.
> No formal verifier can cover all mitigating factors.
> No formal verifier can apply mercy where mercy is needed.
"but the machine will never man-splain like a human could"
"the machine can only mech-splain a bit at best"
Some of the very weakest arguments against formal verification in law. Like being anti due process.
While this discussion is fascinating I think we should scale it back a little. Instead of discussing all aspects I'm quite curious about just one.
How would you define "document" in a way that allows for formal verification? Ideally without relying on words that leave room for interpretation.
> But the Rodin Museum and the Ministry of Culture simply ignored the court’s order. To be clear, they did not appeal it, they ignored it.
No formulation of the law will solve this. The problem is clearly not that the law was unclear. Either the people with real power do what's right, or they don't.
It's a tall claim, given a proper formalization (say under democratic control), malicious counterparty just can't force the national formal verifier to pronounce this or that if it doesn't follow.
please don't make this a partisan issue, I'm sure you can come up with ways to fool a minimalistic verifier (redundantly implemented) into agreeing with your position.
Imagine every autocrat or dictator and all agents of the state, having freedoms, would have to prove the law authorizes them to exercise this or that step, instead of dictating orders. Imagine everyone was raised to ignore authority figures and only execute commands that are provably in compliance with the law, raised to double check it by formal verification. It will point out any flaws on the path to the "desired conclusion". If properly grounded it would be hell for control freaks, they'd leave government positions at scale, the real problem solvers (some human, some machines if we cherish human rights etc more than vanity) would float up.
Does that sound it makes life easier or harder on your average boogeyman?
I didn't downvote, I'm just curious who "they" is?
suppose for the sake of argument
1) the Rodin museum wishes to continue receiving funds for culture,
2) the citizen interested in the 3D point cloud has a valid argument (which somehow relies on the fact that 1+1=2)
3) the Rodin museum claims 1+1!=2 and ignores the proof that 1+1=2
4) the democracy had already converted the law into first order logic & set theory form by adding normative or ethical axioms and definitions (it probably even doesn't just define all the axioms and definitions, but even includes example theorems and proofs like "a gypsie also enjoys human rights" or "yes a black human also has human rights" (these would be theorems not extra redundant axioms inserted into the law when this or that extravagant scandal broke out).
With everything set up as above: the citizen asks the Rodin museum for the 3D scans, for some bizarre reason the Rodin museum operators experience an existential nervous breakdown and refuses. The citizen starts assembling a proof that citizens have the right to any data the system generates (besides certain exceptional things like privacy violations or national security). The citizen proceeds to go through the list of exceptions and proves each of them inapplicable (unlike the shape of submarine propellers, the shape of Rodin's statues are not on the national registry of national secrecy). Rodin died in 1917. If any personal privacy data is embedded in the shape of Rodin's statue these people who's privacy is affected are long dead. Any shape modifications that occurred at later dates could theoretically leak private details to the public. Perhaps a vandal inscribed the telephone number of some actress. In that case the Rodin museum is provably a bad custodian, so let's assume the museum was a good Custodian, no privacy violations would occur if they release the 3D shape, and the citizen continues through all the cases and demonstrates no exceptions hold. For some reason the citizen relies on the definition of 2=1+1. If you ask what would probably happen if the Museum just ignores it? It just pretends to be a good museum and decides to sweep the floor again, without obeying to the consequences of the citizen's proof.
Last day of the month, it's Rodin museum's turn to deliver proof of fulfilling their duties, if anyone wants to see pay. They fail to demonstrate completion of all their tasks: that citizen by exercising his provable rights, has automatically inserted a task they refuse to complete. They choose to not earn money... automatically some job positions open, the formally verified government is now looking for a new operator of the Rodin museum.
Thats what I would expect happen if formal verification were embraced in society.
So two issues. Fist, the lack of mathematical rigour in law and policy is generally considered a feature, not a bug. Second, if the state is unwilling to compel action or enforce punishment from/on the entity in the wrong (Rodin in this case) then it does not matter at all how compelling or rigorous the argument is.
Which in Rodin's case is what happened, the author did get a judgement ordering Rodin to turn over the data, they refused, the author then went back to the courts to force them to act. The court decided it didn't want to despite the prior judgement.
> Imagine everyone was raised to ignore authority figures and only execute commands that are provably in compliance with the law,
Ok I can at least see you've thought about this, but this part is not happening. Definitely not this century, probably not ever. Despite our best delusions, we're still just apes who follow other apes, mostly based on social relationships or the appearance of confidence. We can't even train our society to vote.
we don't need to attain this hypothetical perfectly effective education that prevents us from blindly following authority figures: even if we fail at such an education we can simply guard against the corruption of logic by formal verification, we can design the system to be ape-proof.
You can't make it ape-proof because, at minimum, the last mile of enforcement is performed by apes, who are going to continue following their ape instincts. Unless you plan to have government and law enforcement run entirely by robots.
My point is, the "national formal verifier" doesn't enter the picture. The entity in the role of a formal verifier in this story gave the correct answer and it didn't help.
Ah, ok, in that case the only additional insight is that if finance is regulated by law, that any agent of the state if its a judge or a police officer, they can only proceed their work (and accept payment) if they prove their steps are valid, both parties can directly point at proofs or lemmas it has constructed and those will be automatically accepted when valid.
Also this would mean you can verify your claims at home and have the same software running locally verify if the verifier-as-a-judge will accept or reject your proof before you even submit it.
I'm not upset, but what you're proposing is just stupid. If you think that mathematical formalization is a desirable quality then you clearly don't understand the purpose of having a legal system in the first place.
Are laws expected to be completely self and cross consistent?
I wanted programmatic law in the past and then after thinking and talking a bit, concluded that self and cross consistency in the law is not considered necessary.
Obviously a formal verifier metamath, and a corresponding database like set.mm but law.mm containing all the normative statements etc would have to be supported by an ecosystem, such an ecosystem should reward finding inconsistencies, since if we tolerate just one inconsistency (which would correspond to true == false) then every statement provably true can be proven false and vice versa, this is the principle of explosion: a formal system loses every meaning when an inconsistency is present, hence an ecosystem maintaining the law would encourage finding inconsistencies instead of swiping the arbitrarianism under the rug.
It can't be completely self and cross consistent, it's not possible. But that is exactly the goal, we just can't achieve it.
How do you know if you are breaking the law or not if it's inconsistent? And like the sibling points out, any inconsistency can be abused to declare you guilty or innocent on any behavior depending on the partisanship and interests of the judge.
I used to want programmatic law for exactly the reason that I could determine what was illegal so I didn't break the law.
After a while and talking to smart people I became convinced that was impossible; instead, we have a judicial system filled with experts who make heuristic decisions, and (ideally) it's biased towards not finding people guilty of breaking complex laws they couldn't have figured out. Life requires flexible thinking.
Legal systems typically use non-monotonic logic. Most formal logic systems, particularly in mathematical fields, use monotonic logic. Monotonic logic isn't well suited for the law or most other areas of human activity.
If you want an entire legal system formally defined in logic, you're going to have to do a ton of novel work in expanding the understanding of and application of non-monotonic logic because there isn't much scholarship compared to monotonic logic systems.
That said, France is one of the only countries that has tried anything like this. Their tax system is required to be defined and expressed algorithmically, and they even built a programming language and compiler tool chain to do this. I think it uses monotonic logic, though, and I don't think anybody has seriously suggested the French tax code is something to be copied, neither as a tax code nor an approach to legal codification more generally.
> Their tax system is required to be defined and expressed algorithmically, and they even built a programming language and compiler tool chain to do this.
That's a very interesting fact. Especially in the context of the recent news of the 50 billion euros deficit <a href="https://www.cnbc.com/2026/09/24/france-budget-debt-deficit-government.html" rel="nofollow">https://www.cnbc.com/2026/09/24/france-budget-debt-deficit-g...
If their taxes are defined mathematically I would not expect constant mishaps with the budget.
> People always get upset when I propose mathematical formalization of law and using e.g. metamath verifier as a judge.
I don’t get upset. I just don’t know what that means. What would that look like in practice?
Lets see some simple example. 18 U.S. Code § 912: “Whoever falsely assumes or pretends to be an officer or employee acting under the authority of the United States or any department, agency or officer thereof, and acts as such, or in such pretended character demands or obtains any money, paper, document, or thing of value, shall be fined under this title or imprisoned not more than three years, or both.”
How would you write that in mathematical formalization?
And then how would you make a metamath verifier judge if Robert J. Rippee committed it on
January 1, 1991? I’m sure you can google the case(United States v. Rippee, 961 F.2d 677), but a short summary: “On January 1, 1991, officers from the National City, Illinois, Police Department stopped Rippee for making an illegal U-turn. The officers let Rippee go without a ticket, however, when he told them he was a United States Marshal on his way to break up a fight at Fannies' Night Club in Brooklyn, Illinois. […] Rippee stipulated that he was not and had never been a United States Marshal.“
How would something like that look like under your proposed system?
> I don’t get upset. I just don’t know what that means.
metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:
1) the formal verifier (there are multiple re implementations)
2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)
3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons
A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.
Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.
If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").
Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?
Can you walk through the process for the proposed example?
The problem in most suites is checking if a specific act in real life meets some definition of a crime and not figuring out the wording of the law, right?
You kill someone without a reasonable excuse -> You get punished x years for murder
wouldn't really make murder trials easier because you would still have to formalize what you put into the proof.
Other than genuine self defense, I disagree with every single “justification” you listed. So yes, in my eyes (and the eyes of many other people I expect), the law could be substantially simplified.
You can disagree but no one has to care...unless you can mobilize an army.
Anyway it seems like much of this discussion presupposes the virtue of law and or has amnesia regarding its origins and its service to power. Sure there are exceptions, not every civilization has turned into a tinpot dictatorship because they adopted having a legal system. But without exception, it's those in power who make the rules. And quite often the powerful make rules that benefit them...often benefitting them exclusively.
I would rather live in a society with just laws than not, but again who settles what is just and what is not? Some people clearly have very different ideas. And yet geopolitics and world history aren't determined by the discourse.
And anyway, the law and justice are two different things. Many judges and attorneys will tell you so, I've known more than a few.
I don't get upset. I just know that you have no idea what you're talking about. Talk to some tech native, smart, practicing lawyers for an hour about this.
"I'm right until you get me a conversation with Terence Tao".
Sorry, a random stranger on the internet is not going to spoonfeed you. You need to do the work to enlighten yourself.
You don't need a lawyer "well versed in metamath". You're being elitist and dismissing perfectly competent experts who know more than enough to demolish your ideas.
DoctorOetker · · focus · HN ↗
At least the metamath verifiers will not bend over backwards and come up with absurd inconsistent counterarguments.
It's the most humiliating thing for citizens when the legal cadre of a nation pretends in the national journal that everybody falls for its lies... openly mocking the concept of truth itself with absurdism.
shiandow · · focus · HN ↗
DoctorOetker · · focus · HN ↗
I'm not sure what this sentence even means, of course the democracy should have define those.
its up to the electorate to democratically define what is a document, to define classifications of types of documents, and which ones are administrative.
> The judges main task is formalising reality and lawd, the rest of the inference is typically easy.
Except the judge is plainly ignoring valid derivations, and as a verifier making silly "proofs" up (civil law, not common law) in full-frontal-nudity on behalf of one party.
The problem is not the concept of law, nor the concept of democracy, nor the concept of formalization: the problem is how do we defend against and formalize a response to corrupt verifiers in the legal system?
Those who understand technology to verify arguments already exists can only come to the conclusion we'd be better of with formal verifiers in legal systems.
drysart · · focus · HN ↗
Those who understand law know that formal verifiers cannot replace a judge, because every facet of law (the writing of it, the interpretation of it, the application of it, and the enforcement of it) has to account for all the vagueries of human existence.
No formal verifier can account for definitions that need to expand as the scope of human endeavor expands. No formal verifier can determine mens rea. No formal verifier can determine if something is obscene. No formal verifier can determine someone's mental competence. No formal verifier can cover all mitigating factors. No formal verifier can apply mercy where mercy is needed.
DoctorOetker · · focus · HN ↗
Not the vagueries of human existence, only vagueries of law specified in natural language.
> No formal verifier can account for definitions that need to expand as the scope of human endeavor expands.
No formal verifier is expected to account for definitions, the democracy shapes the law, and the law would first need to be rewritten as definitional axioms in the database of axioms, theorems & proofs. The verifier is just a minimalistic algorithm performing substitution maps on sequences of tokens. This is intentionally minimalistic to minimize the error / attack surface on the verifier itself.
(Currently only error hardening has happened for metamath verifiers, so obviously we would want formal proofs of the absence of 0-days in the verifier)
> No formal verifier can determine mens rea.
It's up to the democratic population while formalizing, to either formally define intent (which presumably goes nowhere), or to pragmatically accept that in the absence of external traces of intent the only thing society can do is define action-reaction patterns, not intention-reaction patterns, but again, that's not the formal verifier, but the database of axioms, definitions (and theorems and proof)
> No formal verifier can determine if something is obscene.
The same, if democracy by referring to a concept of "obscene" chooses to place itself in the position of needing to first define "obscene" in the database of axioms and definitions. But no formal verifier needs to determine this, the verifier just checks a proof in a due process fashion.
> No formal verifier can determine someone's mental competence.
The formal (not natural langue) law could specify how to assess mental competence in a secure non-malleable way (if the democracy decides it needs that). I'm not a dictator, it's not up to me to propose the exact definitions. The formal verifier is not the place to handle these issues, those should reside in the database of axioms and definitions.
> No formal verifier can cover all mitigating factors.
> No formal verifier can apply mercy where mercy is needed.
"but the machine will never man-splain like a human could"
"the machine can only mech-splain a bit at best"
Some of the very weakest arguments against formal verification in law. Like being anti due process.
shiandow · · focus · HN ↗
How would you define "document" in a way that allows for formal verification? Ideally without relying on words that leave room for interpretation.
andrewflnr · · focus · HN ↗
No formulation of the law will solve this. The problem is clearly not that the law was unclear. Either the people with real power do what's right, or they don't.
DoctorOetker · · focus · HN ↗
It's a tall claim, given a proper formalization (say under democratic control), malicious counterparty just can't force the national formal verifier to pronounce this or that if it doesn't follow.
miohtama · · focus · HN ↗
DoctorOetker · · focus · HN ↗
Imagine every autocrat or dictator and all agents of the state, having freedoms, would have to prove the law authorizes them to exercise this or that step, instead of dictating orders. Imagine everyone was raised to ignore authority figures and only execute commands that are provably in compliance with the law, raised to double check it by formal verification. It will point out any flaws on the path to the "desired conclusion". If properly grounded it would be hell for control freaks, they'd leave government positions at scale, the real problem solvers (some human, some machines if we cherish human rights etc more than vanity) would float up.
Does that sound it makes life easier or harder on your average boogeyman?
MadnessASAP · · focus · HN ↗
DoctorOetker · · focus · HN ↗
suppose for the sake of argument
1) the Rodin museum wishes to continue receiving funds for culture,
2) the citizen interested in the 3D point cloud has a valid argument (which somehow relies on the fact that 1+1=2)
3) the Rodin museum claims 1+1!=2 and ignores the proof that 1+1=2
4) the democracy had already converted the law into first order logic & set theory form by adding normative or ethical axioms and definitions (it probably even doesn't just define all the axioms and definitions, but even includes example theorems and proofs like "a gypsie also enjoys human rights" or "yes a black human also has human rights" (these would be theorems not extra redundant axioms inserted into the law when this or that extravagant scandal broke out).
With everything set up as above: the citizen asks the Rodin museum for the 3D scans, for some bizarre reason the Rodin museum operators experience an existential nervous breakdown and refuses. The citizen starts assembling a proof that citizens have the right to any data the system generates (besides certain exceptional things like privacy violations or national security). The citizen proceeds to go through the list of exceptions and proves each of them inapplicable (unlike the shape of submarine propellers, the shape of Rodin's statues are not on the national registry of national secrecy). Rodin died in 1917. If any personal privacy data is embedded in the shape of Rodin's statue these people who's privacy is affected are long dead. Any shape modifications that occurred at later dates could theoretically leak private details to the public. Perhaps a vandal inscribed the telephone number of some actress. In that case the Rodin museum is provably a bad custodian, so let's assume the museum was a good Custodian, no privacy violations would occur if they release the 3D shape, and the citizen continues through all the cases and demonstrates no exceptions hold. For some reason the citizen relies on the definition of 2=1+1. If you ask what would probably happen if the Museum just ignores it? It just pretends to be a good museum and decides to sweep the floor again, without obeying to the consequences of the citizen's proof.
Last day of the month, it's Rodin museum's turn to deliver proof of fulfilling their duties, if anyone wants to see pay. They fail to demonstrate completion of all their tasks: that citizen by exercising his provable rights, has automatically inserted a task they refuse to complete. They choose to not earn money... automatically some job positions open, the formally verified government is now looking for a new operator of the Rodin museum.
Thats what I would expect happen if formal verification were embraced in society.
MadnessASAP · · focus · HN ↗
Which in Rodin's case is what happened, the author did get a judgement ordering Rodin to turn over the data, they refused, the author then went back to the courts to force them to act. The court decided it didn't want to despite the prior judgement.
andrewflnr · · focus · HN ↗
Ok I can at least see you've thought about this, but this part is not happening. Definitely not this century, probably not ever. Despite our best delusions, we're still just apes who follow other apes, mostly based on social relationships or the appearance of confidence. We can't even train our society to vote.
DoctorOetker · · focus · HN ↗
we don't need to attain this hypothetical perfectly effective education that prevents us from blindly following authority figures: even if we fail at such an education we can simply guard against the corruption of logic by formal verification, we can design the system to be ape-proof.
andrewflnr · · focus · HN ↗
andrewflnr · · focus · HN ↗
DoctorOetker · · focus · HN ↗
Also this would mean you can verify your claims at home and have the same software running locally verify if the verifier-as-a-judge will accept or reject your proof before you even submit it.
nradov · · focus · HN ↗
dekhn · · focus · HN ↗
I wanted programmatic law in the past and then after thinking and talking a bit, concluded that self and cross consistency in the law is not considered necessary.
DoctorOetker · · focus · HN ↗
marcosdumay · · focus · HN ↗
How do you know if you are breaking the law or not if it's inconsistent? And like the sibling points out, any inconsistency can be abused to declare you guilty or innocent on any behavior depending on the partisanship and interests of the judge.
dekhn · · focus · HN ↗
After a while and talking to smart people I became convinced that was impossible; instead, we have a judicial system filled with experts who make heuristic decisions, and (ideally) it's biased towards not finding people guilty of breaking complex laws they couldn't have figured out. Life requires flexible thinking.
wahern · · focus · HN ↗
If you want an entire legal system formally defined in logic, you're going to have to do a ton of novel work in expanding the understanding of and application of non-monotonic logic because there isn't much scholarship compared to monotonic logic systems.
That said, France is one of the only countries that has tried anything like this. Their tax system is required to be defined and expressed algorithmically, and they even built a programming language and compiler tool chain to do this. I think it uses monotonic logic, though, and I don't think anybody has seriously suggested the French tax code is something to be copied, neither as a tax code nor an approach to legal codification more generally.
betaby · · focus · HN ↗
That's a very interesting fact. Especially in the context of the recent news of the 50 billion euros deficit <a href="https://www.cnbc.com/2026/09/24/france-budget-debt-deficit-government.html" rel="nofollow">https://www.cnbc.com/2026/09/24/france-budget-debt-deficit-g...
If their taxes are defined mathematically I would not expect constant mishaps with the budget.
thyrsus · · focus · HN ↗
krisoft · · focus · HN ↗
I don’t get upset. I just don’t know what that means. What would that look like in practice?
Lets see some simple example. 18 U.S. Code § 912: “Whoever falsely assumes or pretends to be an officer or employee acting under the authority of the United States or any department, agency or officer thereof, and acts as such, or in such pretended character demands or obtains any money, paper, document, or thing of value, shall be fined under this title or imprisoned not more than three years, or both.”
How would you write that in mathematical formalization?
And then how would you make a metamath verifier judge if Robert J. Rippee committed it on January 1, 1991? I’m sure you can google the case(United States v. Rippee, 961 F.2d 677), but a short summary: “On January 1, 1991, officers from the National City, Illinois, Police Department stopped Rippee for making an illegal U-turn. The officers let Rippee go without a ticket, however, when he told them he was a United States Marshal on his way to break up a fight at Fannies' Night Club in Brooklyn, Illinois. […] Rippee stipulated that he was not and had never been a United States Marshal.“
How would something like that look like under your proposed system?
DoctorOetker · · focus · HN ↗
metamath is an open source formal verification system, the current metamath project (not focussed on law, but mathematics) has roughly 3 parts:
1) the formal verifier (there are multiple re implementations)
2) the databases of axioms (including definitions), theorems and proofs: currently most math is in set.mm the database for set theory (which includes numbers, etc)
3) documentation, among which a thorough book describing how the formal verifier works, the book is creative commons
A proof is basically a series of invocations (by label) of axioms, or previously concluded facts or rules, in the right order so that the verifier comes to the desired conclusion. The algorithm performs all the substitutions and after the last invocation either the string it arrived at matches the proclaimed theorem or it doesn't. Of course it can also error out earlier, say if an invocation to an unknown label happened.
Precisely because natural language is ambiguous, the conversion of our natural laws into formal ones would have to happen under democratic control.
If academic mathematicians want to preserve a human mathematical academy in the face of governments potentially making the future mistake of abolishing mathematical academia, their strong move would be for them to define a "government for and by mathematicians", the database would contain definitions of their choosing, formally regulating how to award public funds into research, formalizing front-running resistant timestamping of work-in-progress etc, so that mathematicians can freely talk and communicate advances ("just wait a sec, let me sync my insights with the network first, ... aaand done, ok now I can speak freely").
Ultimately from a survival perspective, which type of system do we believe to be more robust against corruption and conflicts of interest? one where due process is formally defined in a rigorous manner? or one where those who corrupt the system happen to corrupt it towards actual progress?
echoangle · · focus · HN ↗
The problem in most suites is checking if a specific act in real life meets some definition of a crime and not figuring out the wording of the law, right?
You kill someone without a reasonable excuse -> You get punished x years for murder
wouldn't really make murder trials easier because you would still have to formalize what you put into the proof.
MisterMunchkin · · focus · HN ↗
Consider a simple crime, murder. Let’s simplify it to “if you kill someone, that’s murder and you get life”
But then what if I’m being stabbed by the person I kill?
Okay so self defence.
But then what if I say it’s self defence but factually that’s incorrect, but I genuinely believed it was self defence?
What if I’m a soldier and I’m shooting an enemy?
What if I shoot them because they’re raping my child?
What if I’m shooting them because they raped my child ten years ago and I’ve been plotting my revenge ever since?
What if someone said they’ll shoot me if I didn’t shoot them?
What if I was in psychosis and thought they were going to kill me?
What if I thought they were a deer and shot them by mistake while hunting?
It turns out we have all these laws in this particular way because of thousands of years of work dealing with all of these issues.
p-e-w · · focus · HN ↗
2muchcoffeeman · · focus · HN ↗
And if you can’t sympathise with any of those cases, I hope you’re never called upon to decide anything involving other people.
bird0861 · · focus · HN ↗
Anyway it seems like much of this discussion presupposes the virtue of law and or has amnesia regarding its origins and its service to power. Sure there are exceptions, not every civilization has turned into a tinpot dictatorship because they adopted having a legal system. But without exception, it's those in power who make the rules. And quite often the powerful make rules that benefit them...often benefitting them exclusively.
I would rather live in a society with just laws than not, but again who settles what is just and what is not? Some people clearly have very different ideas. And yet geopolitics and world history aren't determined by the discourse.
And anyway, the law and justice are two different things. Many judges and attorneys will tell you so, I've known more than a few.
RobotToaster · · focus · HN ↗
zulban · · focus · HN ↗
DoctorOetker · · focus · HN ↗
If you are able to arrange such a discussion, I am genuinely interested!
zulban · · focus · HN ↗
Sorry, a random stranger on the internet is not going to spoonfeed you. You need to do the work to enlighten yourself.
You don't need a lawyer "well versed in metamath". You're being elitist and dismissing perfectly competent experts who know more than enough to demolish your ideas.