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