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

121–130 of 171 posts

Re: The presumption that computers are working correctly

#121

Post by auggierose »

gwd wrote: post #117
auggierose wrote: post #68

Earlier quoted context omitted.

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?

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

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.

Re: The presumption that computers are working correctly

#122

Post by auggierose »

PartiallyTyped wrote: post #86
auggierose wrote: post #68

Earlier quoted context omitted.

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

Re: The presumption that computers are working correctly

#123

Post by auggierose »

xyzzy123 wrote: post #80
auggierose wrote: post #68

Earlier quoted context omitted.

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…

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.

Re: The presumption that computers are working correctly

#124

Post by jpc0 »

zubairq wrote: post #120
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…

Thanks for the detailed answer. I think however that the real reason that there is a big industry to find and solve bugs is because of decision made when building and designing the software in the first place. For example if software was built in a robust way with care taken to refactor code along the way then maintenance and bug fixing would probably be a lot easier and may not need an entire industry to support it

I would hope so but I don't think that is the case, there is a portion of bugs, including security vulnerabilities that are actually hardware related but has a workaround in software.

That and no matter how hard you try there will always be logic errors in programming that will need to be fixed.

Re: The presumption that computers are working correctly

#125

Post by KaiserPro »

jfoutz wrote: post #8

How does that work? I'm not a lawyer. I'm a lazy programmer. So, does the defense get to subpoena the logs, and depose a programmer to explain why some random request returned a 502? Does the defense get, like, red team access? Although I'm a lazy programmer, I do think a lot about failure modes. If my freedom is on the line, I can probably think up a few (orders of magnitude) test cases. Happy to provide a shell scr…

its divide and conquer and abuse of power.

The post office found that money was "missing". It went after the sub-postmasters. The sub-postmasters didn't know that it was a systemic issue, they were told to plead guilty to reduce their sentence.

Unless you have a credible lawyer, and have a clue that something in the system might be wrong, then you're not going to know.

Re: The presumption that computers are working correctly

#126

Post by zubairq »

jpc0 wrote: post #124
zubairq wrote: post #120

Earlier quoted context omitted.

Thanks for the detailed answer. I think however that the real reason that there is a big industry to find and solve bugs is because of decision made when building and designing the software in the first place. For example if software was built in a robust way with care taken to refactor code along the way then maintenance and bug fixing would probably be a lot easier and may not need an entire industry to support it

I would hope so but I don't think that is the case, there is a portion of bugs, including security vulnerabilities that are actually hardware related but has a workaround in software. That and no matter how hard you try there will always be logic errors in programming that will need to be fixed.

Yes that is actually a very good point, I stand corrected

Re: The presumption that computers are working correctly

#127

Post by kazinator »

checkyoursudo wrote: post #74
kazinator wrote: post #27

Every prosecutor in possession computer evidence of a crime having to prove the software correct is a nonstarter. Assuming it's right, and proving it buggy, is the right principle.

This is contrary to the principle of presumed innocence. This is presumed guilt. The burden should always be on the prosecution to prove guilt, and if that requires the prosecution to prove the correctness of hardware, models, software, or data, then that is what should be required. And if the prosecution cannot prove the legitimacy of evidence, then than evidence should be disallowed. The standard does not have to b…

> This is contrary to the principle of presumed innocence.

No it isn't. It just means that some situation involving information from computers is "circumstantial evidence".

If programs have to be proved correct, that basically means data from computers could never be introduced as circumstantial evidence.

For instance, guns are normally assumed not to go off unless someone pulls the trigger. If a member of the Crips guns down a Bloods member across the street, he could claim that his gun accidentally went off the moment he was inadvertently pointing a gun in the direction of the enemy gang member. If he could prove that true, then it could be ruled an accidental death. If the defense lawyer does not make that argument, it will be assumed that there was nothing wrong with the gun, and thus someone pulled the trigger.

Re: The presumption that computers are working correctly

#128

Post by PartiallyTyped »

auggierose wrote: post #122
PartiallyTyped wrote: post #86

Earlier quoted context omitted.

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:

Re: The presumption that computers are working correctly

#129

Post by citizenpaul »

bostik wrote: post #73
bmitc wrote: post #40

Earlier quoted context omitted.

> I’m often surprised that computer systems work at all. I also remain contunually amazed that anything works. It boggles my mind, because I have seen how software gets built. How can it possibly all work? I think my answer to this conundrum and seeming paradox is that it doesn't all work. We have trained ourselves and been trained to accept things that aren't working as something else. And like you say, people treat…

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 not only did their online portal not have controls to make sure that internal money transfers are confirmed before processing. They also had no controls to make sure that when an internal transfer is done that the money is there to be transferred.

I waited a couple days expecting a call. Nope. At the end of week I call them. Get transferred around a bunch. The whole time everyone is saying everything is good nothing is wrong, there is no problem. I 100% certain every single one of them was lying through their teeth while they go the FBI on the phone because of the automatic assumption that the computers are right and I am automatically a criminal. There is no way all those people saw a -200k balance in a saving account and thought it was fine. (BTW that means it is standard bank policy to lie to a customer when something is wrong)

So what happened. They immediately zeroed my accounts and froze all my bank activity for three months while they "investigated" Then they only returned 15K of the original 20k that I moved so they effectively stole 5k from me. I spend another 6 months trying to get that money back and did not succeed.

I would have been screwed if I had not been born poor and was familiar with the banking system corruption. I have my income,spending,saving and investing split among different banks and banks accounts in case of something like this ever happened.

The bank initials are WF.

Re: The presumption that computers are working correctly

#130

Post by kazinator »

jpc0 wrote: post #57
zubairq wrote: post #43

Earlier quoted context omitted.

I’m quite interested to learn and understand the line of reasoning for this comment. Care to elaborate?

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.

Post reply on HN