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.
alt Hacker News
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.