Proposition: "They either do not use private code or they did something very very stupid."
Proof: "Not using private code is very easy (for example google does not train its models on workspace users' data, which is why they get inferior features) and they promised multiple time not to use private code so doing in would be hard to justify"
> It means no one ever ran those instructions and checked the result.
That's not really true. It means they produced wrong values with some input. They may have tested but not hit the pathological input case. No one is going to sweep the entirety of the domain. You really need a formal proof to avoid these bugs.
If we suppose that his conclusion is using boolean logic, then what you're saying is a strawman because of his last claim; namely, protobufs are bad if "[...] && !Google":
> They're clearly written by amateurs, unbelievably ad-hoc, mired in gotchas, tricky to compile, and solve a problem that nobody but Google really has.
This dovetails with other arguments that I've seen recently that are becoming more frequent:
Have we entered a new world where the lessons of companies working at massive scales are not only generally superfluous for smaller scales, but are actively harmful?
The reason they don't train the model on their code is specifically because they don't want it accidentally spitting out snippets of their proprietary code, not because the code is "extremely hard to work with."
I'm amazed you called that argument silly while countering with this.
> is it not reasonable to assume that the number of security flaws just reflects how insecure most public code is?
It sounds to me like that's not an inference that can easily be drawn. Copilot was trained on predicting code, it doesn't understand the code it produces syntactically. Security issues can be highly context dependent. For example, in most cases it's fine to log a variable, but when it happens to contain a password, it's a security issue. This is a flawed example as the algorithm may be able to learn that variables with names or contexts suggesting that they're secrets should not be logged, but I can imagine much more subtle issues can crop up.
> He clearly hasn't proven anything about his code.
Is that a bad thing? It seems like many people are able to write software that works well and gets the job done without "proving anything" about their code in the way you're describing. Personally, I'm fine with not proving anything if I can deliver quickly and everything works, but I'd like to be convinced otherwise if there's real value there.
Since tomp objects to trusting code, then I agree with
Manishearth: if you're never willing to trust code, then you can never have guarantees. Even the proof engine is trusted code.
>If we found bug x, y and z will necessarily be found, therefore VeraCrypt is insecure.
I did not make that argument, I made a probabilistic argument. Trying to apply deductive logic fallacies to probabilistic arguments is a type error.
>if you can't identify or find them, you can't claim they exist.
I made no absolute claim about the existence or nonexistence of bugs, only about the expected number of bugs, that is, a probabilistic estimate.
> There's no such thing as a bug "hit rate".
Of course there is, it is, trivially, the number of bugs found by the audit / the total number of bugs.
Look at this way: I have two auditors, Alice and Charles. Charles is known to be pretty sloppy, he looks over code quickly, skip parts, etc, but the bugs he finds are usually actual bugs. Alice is extremely rigorous and misses very few bugs.
I have 2 pieces of software, SuperCrypt and UltraCrypt.
Charles audits SuperCrypt and finds 137 critical bugs. He audits UltraCrypt and finds only one.
I know Alice will review both code bases next week. Where do you think she'll find more bugs?
Yeah, people fixated on the meaning of "makes no sense" to evade accepting that the proofs LLMs output are not useful at all.
On a similar fashion, almost all LLM created tests have negative value. They are just easier to verify than proofs, but even the bias into creating more tests (taken from the LLM fire hose) is already harmful.
I am almost confident enough to make a similarly wide claim about code. But I'm still collecting more data.
The overwhelming majority of the population doesn't have the capacity to understand what you wrote or why that is true. Even the majority of those who understand why it may be true, cannot say for certain that it is true without inspecting the codebase and its operation. That's a major problem.
Where did I assert something similar to your example? It seems like a false analogy. The criticism wasn't even that my logic was flawed but that the same argument could somehow be made to justify any user-hostile action.
If the problem in your point of view is that I didn't /prove/ how big of a problem sideloading was then yes, I didn't even attempt to do that. There's a separate subthread on that question.
> Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs.
Serious question: do you really believe that?
> That's just stupid. Show me the studies.
There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.
> The author of the article implicitly equates "statically verified code" with "bug-free code".
Not at all. First, the statements as put here are discrete (boolean even) while I present both "statically verified code" and "bug-freedom" as living on a continuum. Secondly, I don't equate them. If anything, I assume a monotonic, positive relationship between them (strictly speaking not even that. I make pretty clear that the curves could also have whatever shape. But I yield that I am very suggestive in this because I do strongly believe it to be the case). In fact, one of the main points of the argument is that the two are not equal - otherwise, the blue curves I drew would all be straight lines from (0,0) to (1,1). And lastly, none of this is done implicitly. I mention all of this pretty explicitly :)
2) verifying code requires domain knowledge, which implies that the utility of these models is limited to things could write myself if I weren't too lazy. That's hugely constricting.
Proposition: "They either do not use private code or they did something very very stupid."
Proof: "Not using private code is very easy (for example google does not train its models on workspace users' data, which is why they get inferior features) and they promised multiple time not to use private code so doing in would be hard to justify"
reply