5 ms·

Mathematical verification of both hardware and software should be mandatory, at least as long you rely on it for the law. Simple as that. For example, how can y

Mathematical verification of both hardware and software should be mandatory, at least as long you rely on it for the law. Simple as that. For example, how can you trust a photo, when tons of computational photography has been applied to it, and you don't know the exact amount the algorithms can change the photo?

xyzzy123 3y ago
That's not really economic at present, hopefully it will be one day. There are a very small number of verified programs, no mainstream operating systems and no major application suites. We just don't have the technology for it yet. It does not seem very practical to throw out all digital evidence (eg photos and videos) because there is some chance of misprocessing. Who even records in analog today? What corresponding standard would you demand for analog evidence? Even in analog there were film issues, processing issues, noise, smudges, tampering and uncertainty, people have been dealing with these sorts of confounders for a long time. We don't generally require "mathematical certainty" for other types of evidence. Personally I think GP was proposing a reasonably balanced commonsense perspective.
- auggierose 3y ago
  Common sense does not get you very far in a world where any video or audio can be fake, and you cannot really tell which one is and which one isn't. Common sense is officially done for. Bring on the math.
PartiallyTyped 3y ago
That's easy to say, until you've tried to write a provably correct piece of software or tried to do model checking. I have tried to build models for the schemas that databases have, not their implementation, just the schema, and it is difficult AF. Using z3 for this might as well be trying to start a fire with a pair of rocks.
- auggierose 3y ago
  What exactly have you tried to do there? Isn't a schema already a model? What properties did you want your model to have? Yes, in general it is difficult, because then software becomes mathematics. And that's on top of the software doing something useful and what the user wants. But I think we are now getting the tools to get there. You will still need to become a mathematician, though.
  - PartiallyTyped 3y ago
    > What exactly have you tried to do there? Isn't a schema already a model? What properties did you want your model to have? Yes, a schema is a data-model, and a database can tell you whether the row you are trying to insert satisfies the constraints, but it can't tell you whether an instantiation of the database exists, nor can it tell you how to construct it. There are 2 issues here, first proving that an instantiation exists; and second proving that there's a sequence of insertions that satisfy the constraints. Notice that some tables can have non sat constraints. This becomes significantly harder when you are dealing with recursive definitions, cycles in the dependencies, foreign keys that refer different tables across the same constrained columns, type compatibility, and on and on In other words, the space of all databases described by a schema may not even be constructible :upside_down:
    - auggierose 3y ago
      Ok, I understand. So first you want to see your schema as a property on a database (which is just a bunch of tables with data, I guess), and see if there is actually any such database, or if the property is always false. Second, assuming that there are any such databases: Given certain commands which operate on databases, is there any sequence of commands which transform the empty database into a database such that the schema property holds for it? Actually, you probably would want the property to be true for every intermediate step as well, right? Sounds interesting! Although in practice, solving this is probably not that important, because if you cannot come up with some examples of constructing databases for your schema and application, then the schema is the wrong one pretty much by definition.
gwd 3y ago
Come now; imagine a world where nobody could ever be convicted without mathematical verification of all components of evidence. Nobody could be convicted of anything, since even if we had 10 people and three 4k video cameras all see someone pull out a gun and shoot somebody, we can't have mathematical certainty even of the three video cameras, much less the unreliable wetware memories of 10 people. We might as well give up having trials entirely.
- auggierose 3y ago
  I rather rely on the memories of 10 people than on 4K cameras which can be hacked. I don't mind relying on a 4K camera for something like tennis, to decide if a ball is out or not. But if it is just up to software if I go to prison for 10 years or not, I very much DO mind.
  - brokenmachine 3y ago
    I'll take the 4k cameras over eyewitnesses, thanks. Have you ever dealt with the public?
  - ericjmorey 3y ago
    Are you aware of just how unreliable eyewitness testimony is?
    - PartiallyTyped 3y ago
      It's the least reliable form of "evidence". If anything, it's an anecdote at best.
    - auggierose 3y ago
      Yes, and I still prefer it over digital only evidence. Are you aware how totally unreliable digital is?
andrewaylett 3y ago
The rule is either "on the balance of probabilities" or "beyond a reasonable doubt". Neither of which was well-applied in the Horizon cases. "Mathematically proven" is almost always the wrong standard for legal cases, as it doesn't speak to the quality of the proof. The relevant standard ought to have been "beyond a reasonable doubt", but obviously even those who did know better managed to convince the court that doubting the computer was unreasonable. Apparently without manually checking the output against reality, even when the defendent brought their own numbers? I strongly suspect that the racial discrimination that's being revealed by the press played its part in that -- no need to worry about the computer, or even about reality, if one's mind is set anyway.

xyzzy123 3y ago

That's not really economic at present, hopefully it will be one day. There are a very small number of verified programs, no mainstream operating systems and no major application suites. We just don't have the technology for it yet. It does not seem very practical to throw out all digital evidence (eg photos and videos) because there is some chance of misprocessing. Who even records in analog today? What corresponding standard would you demand for analog evidence? Even in analog there were film issues, processing issues, noise, smudges, tampering and uncertainty, people have been dealing with these sorts of confounders for a long time. We don't generally require "mathematical certainty" for other types of evidence. Personally I think GP was proposing a reasonably balanced commonsense perspective.

auggierose 3y ago
Common sense does not get you very far in a world where any video or audio can be fake, and you cannot really tell which one is and which one isn't. Common sense is officially done for. Bring on the math.

PartiallyTyped 3y ago

That's easy to say, until you've tried to write a provably correct piece of software or tried to do model checking. I have tried to build models for the schemas that databases have, not their implementation, just the schema, and it is difficult AF. Using z3 for this might as well be trying to start a fire with a pair of rocks.

auggierose 3y ago
What exactly have you tried to do there? Isn't a schema already a model? What properties did you want your model to have? Yes, in general it is difficult, because then software becomes mathematics. And that's on top of the software doing something useful and what the user wants. But I think we are now getting the tools to get there. You will still need to become a mathematician, though.
- PartiallyTyped 3y ago
  > What exactly have you tried to do there? Isn't a schema already a model? What properties did you want your model to have? Yes, a schema is a data-model, and a database can tell you whether the row you are trying to insert satisfies the constraints, but it can't tell you whether an instantiation of the database exists, nor can it tell you how to construct it. There are 2 issues here, first proving that an instantiation exists; and second proving that there's a sequence of insertions that satisfy the constraints. Notice that some tables can have non sat constraints. This becomes significantly harder when you are dealing with recursive definitions, cycles in the dependencies, foreign keys that refer different tables across the same constrained columns, type compatibility, and on and on In other words, the space of all databases described by a schema may not even be constructible :upside_down:
  - auggierose 3y ago
    Ok, I understand. So first you want to see your schema as a property on a database (which is just a bunch of tables with data, I guess), and see if there is actually any such database, or if the property is always false. Second, assuming that there are any such databases: Given certain commands which operate on databases, is there any sequence of commands which transform the empty database into a database such that the schema property holds for it? Actually, you probably would want the property to be true for every intermediate step as well, right? Sounds interesting! Although in practice, solving this is probably not that important, because if you cannot come up with some examples of constructing databases for your schema and application, then the schema is the wrong one pretty much by definition.

gwd 3y ago

Come now; imagine a world where nobody could ever be convicted without mathematical verification of all components of evidence. Nobody could be convicted of anything, since even if we had 10 people and three 4k video cameras all see someone pull out a gun and shoot somebody, we can't have mathematical certainty even of the three video cameras, much less the unreliable wetware memories of 10 people. We might as well give up having trials entirely.

auggierose 3y ago
I rather rely on the memories of 10 people than on 4K cameras which can be hacked. I don't mind relying on a 4K camera for something like tennis, to decide if a ball is out or not. But if it is just up to software if I go to prison for 10 years or not, I very much DO mind.
- brokenmachine 3y ago
  I'll take the 4k cameras over eyewitnesses, thanks. Have you ever dealt with the public?
- ericjmorey 3y ago
  Are you aware of just how unreliable eyewitness testimony is?
  - PartiallyTyped 3y ago
    It's the least reliable form of "evidence". If anything, it's an anecdote at best.
  - auggierose 3y ago
    Yes, and I still prefer it over digital only evidence. Are you aware how totally unreliable digital is?

andrewaylett 3y ago

The rule is either "on the balance of probabilities" or "beyond a reasonable doubt". Neither of which was well-applied in the Horizon cases. "Mathematically proven" is almost always the wrong standard for legal cases, as it doesn't speak to the quality of the proof. The relevant standard ought to have been "beyond a reasonable doubt", but obviously even those who did know better managed to convince the court that doubting the computer was unreasonable. Apparently without manually checking the output against reality, even when the defendent brought their own numbers? I strongly suspect that the racial discrimination that's being revealed by the press played its part in that -- no need to worry about the computer, or even about reality, if one's mind is set anyway.