Comment by gwd | Hacker News Reader

Comment by gwd | Hacker News Reader

Parent Full thread

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.

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?

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.

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.

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.

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.

Are you aware of just how unreliable eyewitness testimony is?

Yes, and I still prefer it over digital only evidence. Are you aware how totally unreliable digital is?

It's the least reliable form of "evidence". If anything, it's an anecdote at best.

I'll take the 4k cameras over eyewitnesses, thanks.

Have you ever dealt with the public?

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.

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.

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.

> 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:

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.

You needn’t think of databases as tables and data, you may think of them as trees of structs, ie an object relational model and show satisfiability of the model by constructing a tree of dependencies.

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.

Now I am interested in what exactly your use case is :-) Maybe you would want to model this first in a general purpose interactive prover such as Isabelle, and proceed from there. But in the end you seem to be looking for a push-button algorithm for proving the consistency of a particular logic, and I can tell you, that's probably not gonna end well.

I can't say much more unfortunately, not yet at least.

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.

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-figh...

> 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.

Reply on news.ycombinator.com