But software.... software gets things wrong all the time and the computer hardware just blindly does what the software told it to.
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?
> But software.... software gets things wrong all the time and the computer hardware just blindly does what the software told it to.
That's not a distinction that's relevant to this article. By "computer" it means a system composed of hardware and software (and which is almost always what "computer" is used to mean):
> The presumption that computers are presumed to be operating correctly, unless there is evidence to the contrary is what lawyers call “a presumption of evidence”.
> This means that a court can be satisfied that a relevant fact can be established just by computer records, unless there is evidence that the computer is not working properly.
> And so when the computer record shows, for instance, a financial shortfall by postmaster or postmistress, the court will accept that as evidence of an actual shortfall - unless the defendant can show that the computer was not operating correctly.
> In short, when the computer record is the essence of a prosecution case: computer says guilty.
Oh you sweet summer child. Hardware has so many little "quirks' or hacks to make it work correctly and it often doesn't! It's often expected that really low-level, "touching the metal" software makes up for these little bumps that happen quite often.
“The Intel Pentium series of CPUs had two well-known bugs discovered after it was brought to market, the FDIV bug affecting floating point division which resulted in a recall in 1994, and the F00F bug discovered in 1997 which causes the processor to stop operating until rebooted.”
You reminded me of the Things I Won't Work With piece that observed in passing that the behavior of dioxygen difluoride was surprisingly well described by its chemical formula. ( https://www.science.org/content/blog-post/things-i-won-t-wor... )
It also leads to the same horrible misjudgements as in the article mentioned above. If you dont know what to look for you will come to erroneous convictions by ruling out the error cases you do know.
Wow there are some patronising people responding to your comment.
I think this is mostly true for 95% of software and the experience of software developers. But CPUs are full of bugs that only manifest when certain code is run - perhaps the order of instructions or when in certain states. Often these are hidden/fixed in software - compilers/drivers/microcode etc.
By hardware do you mean CPU?
Also, these days, "hardware" is still something that's either got a microcontroller, FPGA, or some other thing that is eother running or was designed with software. The area is quite muddy, especially if you deal with hardware systems of a collection of various computers and hardware components.
And I'm not so sure things aren't CPU or IC bugs that get bubbled up. The amount of Heisenbugs and various other transient bugs make me question that.
In my experience with instrument control systems, the bug could be anywhere from a cable to the UI or anything in between. These systems had to be developed in strict layers to help isolate bugs and also workaround them.
too broad a generalization i think.
who told these computers to do what they did?
https://www.bbc.com/future/article/20221011-how-space-weathe....
Hardware people are fully aware of their shortcomings, but they also are fully aware that software is even worse.
Far far worse.
Here is just one example to get you started: https://nakedsecurity.sophos.com/2011/08/10/bh-2011-bit-squa...
https://edc.intel.com/content/www/us/en/secure/design/confid...
Hardware bugs are simply capsuled better so people dont recognize them as such. Its the same mechanism at play as for people who assume software normally functions. They are also just unaware of the inner working.
Stuff is just really complicated and people should manage their expectations. I get that going from assuming to have a solid base to no such thing existing is difficult to handle but there is no sensible way around that. Not doing so gets you stuff like the article.
I am having quite the big problem with this getting downvoted. The poster is spot on here and this needs to be communicated. Not doing so is irresponsible. Overconfidence in this regard is extremely dangerous and there is no nicer way to say this.
You can not reasonably assume that you are able to judge something works reliably without understanding how the error cases look. Especially if these are capsuled from you and or you dont know what to look out for.
This is at the very core of why something like the post scandal was possible. People repeating the same mistake in this very thread is just really bad. The only thing worse would be not telling them this.
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...