Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The presumption that computers are working correctly

emptycity.substack.com

Post reply on HN
Print view View original

141–150 of 171 posts

Re: The presumption that computers are working correctly

#141

Post by andrewaylett »

auggierose wrote: post #68
gwd wrote: post #48

Earlier quoted context omitted.

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 h…

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?

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.

Re: The presumption that computers are working correctly

#142

Post by rwmj »

ric2b wrote: post #140
rwmj wrote: post #70

Earlier quoted context omitted.

The real problem is this isn't a "right" that the postmasters could exercise. You're accused of stealing money. You're not paid very much in the first place and have only limited legal aid, and may even be in prison (on remand) already. There's no "defense team", you only have a solicitor assigned to you at the police station. You're also not a programmer. How are you going to argue that the database which shows you…

And the only evidence the prosecution needs to show is some log messages from the system saying the math doesn't add up? Nothing else?

Yes. Try reading the article?

Re: The presumption that computers are working correctly

#143

Post by ploxiln »

citizenpaul wrote: post #129
bostik wrote: post #73

Earlier quoted context omitted.

People outsource their critical thinking all the time, but with computers the failures are more egregious. There is less recourse to correct things, and information propagating through systems can make the error more persistent. Also: people take the verdict from a computer as a given even when reality and computer disagree. I've used this story a couple of times before on HN, and if it hadn't happened to mother's co…

I had a similar experience as your moms colleague. I transferred 20k from savings to checking. During the process I think what happened is the web banking page froze and allowed me to hold the enter key on confirm that repeated several times. I ended up with 200k in my account that came as a negative 180k balance to my saving account sent to my checking account. (values rounded for story simplicity) This meant that n…

+1 to the advice to have different accounts with different banks. I've done this for a bit over 10 years now: checking account at one bank, savings at a different bank, credit card at yet another different bank, yet another credit card at yet another different bank, joint checking account with spouse at yet another different bank ...

My spouse did run into some nonsense some years ago due to her checking and savings accounts being at the same bank and automatically linked and mixed-up. Banks are always offering you super convenient awesome features with "protection" and "connection" and just PLEASE NO - that's how one mistake, that was that bank's in the first place, takes down all your available funds. You'll probably get most back, eventually, but do you really want to live with that for some weeks/months ...

Re: The presumption that computers are working correctly

#144

Post by PartiallyTyped »

auggierose wrote: post #137
PartiallyTyped wrote: post #128

Earlier quoted context omitted.

> 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 instantiat…

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 t…

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.

Re: The presumption that computers are working correctly

#146

Post by dboreham »

kazinator wrote: post #130
jpc0 wrote: post #57

Earlier quoted context omitted.

If bugs were easy to find and solve there wouldn't be an entire highly paid industry to do it. Add to that malicious actors actively trying to work against systems (bank/post office/medical system etc) and it becomes pretty hard to prove that both the software and the data referenced by the software is in fact correct. Now think about the last time a critical piece of data was recorded on paper with a pen/analogue ty…

If programs were easy to prove correct, there wouldn't be a testing and debugging industry. Bugs don't have to be root caused and solved in order to call into question the use of some computer situation as circumstantial evidence. The claimed buggy, externally-visible behavior just has to be reproduced. If there are third-party reports of it, that would help.

> If programs were easy to prove correct

This is just another turtle layer because such proof is only vs a "specification", which turns out to also be a program, written in another language.

Re: The presumption that computers are working correctly

#147

Post by iudqnolq »

envsubst wrote: post #114
dazzawazza wrote: post #78

Earlier quoted context omitted.

There is substantial evidence that the people in power in the Post Office Board dismissed the evidence from the sub post masters because they were, more often than not of Asian descent (Indian, Bangladeshi, Pakistani,...). So the Post Office Board had a mental block to joining the dots because they were racist. When they were eventually confronted with the overwhelming evidence of hundreds of false convictions they d…

> they doubled down because they lack any sense of morality. I don't believe you know what their internal mental states are.

We can and do reasonably infer mental states from actions.

If someone knows they are sending innocent people to prison, benefits from doing so, and continues doing so we can reasonably infer they lack morality.

Re: The presumption that computers are working correctly

#148

Post by auggierose »

PartiallyTyped wrote: post #144
auggierose wrote: post #137

Earlier quoted context omitted.

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 t…

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…

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.

Re: The presumption that computers are working correctly

#149

Post by PartiallyTyped »

auggierose wrote: post #148
PartiallyTyped wrote: post #144

Earlier quoted context omitted.

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…

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.

Re: The presumption that computers are working correctly

#150

Post by zzbn00 »

Spooky23 wrote: post #112
dan-robertson wrote: post #92

Earlier quoted context omitted.

Do you think an increase in punishment the executives expected would have led to the problems for subpostmasters being resolved faster or slower?

Your question makes a good point. Punishment is only effective at the bottom of the funnel. A well designed system, whether a computer or an organization should always have controls that guide things to where they should be. That means carrots and sticks. In a place like a post office, that means separation of duties, audit, and clear lines of accountability. Things fail when nobody asks awkward questions or looks. I…

In principle there was already some separation of duty as solictors in England owe a duty to the Court regardless of who pays them. However it seems not to have been enough in this case. Hopefully will be looked into.
Post reply on HN