As a programmer that works on drivers, it's my experience that hardware almost never works correctly. "We'll fix it in software" might as well be the official motto of the hardware industry.
Also just look at the errata sheet for any microcontroller. Hardware bugs are so prevalent we have a special term and semi standardized document to describe them.
https://apnews.com/article/iphone-15-overheating-apple-softw...
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.
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.
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.
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.
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:
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.
You can do it incrementally for parts of the model, but that doesn’t guarantee that long range dependencies are satisfiable.
Yes, you then need to show that it is incrementally constructible, which is a different can of worms… the tree view above isn’t actually fully correct because you duplicate entries mapping to the same object. Because of this duplication, the tree may refer to an object that can only be inserted later.
Oh and the encoding must be able to accommodate arbitrary length arrays and arbitrary objects … which makes usage of SMT solvers difficult to say the least.
While I agree that for the average company this isn’t useful, and the average engineer won’t shoot their feet on purpose, what I am doing needs to accommodate all those scenarios because I have no guarantees of sanity.
I have semi-sketched the idea in Dafny instead of Isabelle. Direct encoding of arrays makes it difficult, but I am thinking iterative deepening might just work. I am working on a Z3 approach for this, and I am crossing my fingers.
If Z3 doesn't work, I will try emitting Dafny code instead and hooking up to the compiler.
Have you ever dealt with the public?
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.
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-figh...
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.
However when using a computer application and noticing unexpected and erroneous behaviour, what proportion is the time can the bug be traced back to hardware vs software?
I’m going with about 1 to 1000. I think that’s conservative. Do you see it differently?