6 ms·

But thinking about a court case, what should be the presumption? Should it be up to the prosecution to prove that the RAID controller / network card didn't cor

by gwd 3y ago

But thinking about a court case, what should be the presumption? Should it be up to the prosecution to prove that the RAID controller / network card didn't corrupt the data or that the GPU did the math correctly? Or should it be up to the defense to prove that it didn't? And how would each side demonstrate their case to a reasonable level of certainty? As others in this thread have said, for bits of the system that have clearly defined parameters and get extensive testing (by like, millions of people), I think you can begin with the assumption that those bits are correct: you can assume the CPU is adding numbers correctly, that the compiler compiled the code correctly, that the spreadsheet executed the formula it was given correctly, and it's up to the defense to prove otherwise. Bugs in the CPU / compiler / spreadsheet software would get caught pretty quickly. But for bits where the right answer is not clear, and / or doesn't get extensive testing -- the formulas inside the spreadsheet, custom-written software -- the assumption should be that it does not work, and it should be up to the prosecution to demonstrate that the software is working correctly.

auggierose 3y ago
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.
cf141q5325 3y ago
You are treating hardware like software by arguing with the experience we have made so far with a given model. Environmental conditions as well as it being different physical objects is a huge problem for hardware. The data about error cases is also simply not recorded. You get at best statistical reliability with small sounding chances for errors that are still happening all the time. You can also not make any statement about reality by arguing with feasibility. edit: I am unfortunately not qualified to tell you how feasible ways to deal with reality in this case could look. Which doesnt mean that i cant identify some error cases. You also require different levels of competence for designing a rocket and recognizing a non functioning one. edit1: In regards to the usage of statistics as a basis one should also remember confidence and these cases https://www.science.org/content/article/unlucky-numbers-fighting-murder-convictions-rest-shoddy-stats https://www.science.org/content/article/unlucky-numbers-figh...
everforward 3y ago
> the assumption should be that it does not work, and it should be up to the prosecution to demonstrate that the software is working correctly. Phrased differently, you want them to prove there aren't any bugs. You can't prove a negative so this is a non-starter. There will always be "but what if it requires specific timing" or "maybe it relies on some other software being installed" or "maybe the computer had a virus". It's basically the same reason the government has to prove you're guilty; because you can't prove you're not guilty. I think the onus has to be on the defense to prove some kind of a bug exists. The interesting question is whether that implies that the software provider should be required to hand over the source code in discovery. It seems unreasonable to force someone to go on a bug-hunt where their future hangs in the balance without access to the source code. Ditto for providing some kind of a test instance; I can see companies being leery of providing binaries to someone trying to publicly prove there are bugs.

by gwd 3y ago

auggierose 3y ago

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.

cf141q5325 3y ago

You are treating hardware like software by arguing with the experience we have made so far with a given model. Environmental conditions as well as it being different physical objects is a huge problem for hardware. The data about error cases is also simply not recorded. You get at best statistical reliability with small sounding chances for errors that are still happening all the time. You can also not make any statement about reality by arguing with feasibility. edit: I am unfortunately not qualified to tell you how feasible ways to deal with reality in this case could look. Which doesnt mean that i cant identify some error cases. You also require different levels of competence for designing a rocket and recognizing a non functioning one. edit1: In regards to the usage of statistics as a basis one should also remember confidence and these cases https://www.science.org/content/article/unlucky-numbers-fighting-murder-convictions-rest-shoddy-stats https://www.science.org/content/article/unlucky-numbers-figh...

everforward 3y ago

> the assumption should be that it does not work, and it should be up to the prosecution to demonstrate that the software is working correctly. Phrased differently, you want them to prove there aren't any bugs. You can't prove a negative so this is a non-starter. There will always be "but what if it requires specific timing" or "maybe it relies on some other software being installed" or "maybe the computer had a virus". It's basically the same reason the government has to prove you're guilty; because you can't prove you're not guilty. I think the onus has to be on the defense to prove some kind of a bug exists. The interesting question is whether that implies that the software provider should be required to hand over the source code in discovery. It seems unreasonable to force someone to go on a bug-hunt where their future hangs in the balance without access to the source code. Ditto for providing some kind of a test instance; I can see companies being leery of providing binaries to someone trying to publicly prove there are bugs.