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.
> 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.
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.
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.