The main article was discussed at https://news.ycombinator.com/item?id=21433217.
> “When you find a problem in the source code, it’s very difficult to explain the consequences of that problem to a judge or jury,” he told me. “It’s written in a foreign language, and the effects are hard to trace. We’re rarely able to say, ‘Aha, here’s this person’s breath test and here’s the problem that caused it to be wrong.’”
> Mr. Workman’s mind worked a lot like the computer systems into which he delved: He had a mental index of more than 15 years of legal battles and civic investigations into problems with breath-testing programs, and he knew exactly where to find the incendiary bits. When I dug into flawed test results in Washington, D.C., for example, he sent me a video recording of a police officer turned whistle-blower testifying at an oversight hearing.
> With Mr. Workman’s help, I traversed my giant pile of records and filed dozens of Freedom of Information Act requests to fill in blanks. For research on Massachusetts — where more than 36,000 breath tests had been ruled legally inadmissible — Mr. Workman gave me a login to a database he had created containing nearly every one of those tests.
(In fact, the headline, while completely accurate, can be misleading because an unnamed/anonymous source very often refers to a whistleblower or insider, which Mr. Workman is not)
> > “When you find a problem in the source code, it’s very difficult to explain the consequences of that problem to a judge or jury,” he told me. “It’s written in a foreign language, and the effects are hard to trace. We’re rarely able to say, ‘Aha, here’s this person’s breath test and here’s the problem that caused it to be wrong.’”
This is the true power (and 'problem') of Turing Completeness. The effects of any small change are so absurdly non-linear that it's really hard to predict without systems (types, etc.) to constrain us.
Most non-trivial theorems about TMs are un-provable[0], so this should probably come as no surprise, but I find that it's very hard to explain to lay-people just how hard it is to predict what a program will do.
[0] There are some very important and very general ones that are, but that doesn't really matter wrt. predicability in terms of small changes.
Did you mean "conjectures"? Theorems need to be provable by definition, don't they?