Not really. Like, yes, relative to your competitors. But, if the cost of growing potatoes is ten cents per potato, and then I make something that can produce potatoes for one cent then I'd expect everyone to just have more potatoes. This would drive down the cost of potatoes, because the supply would be saturated eventually, but AI is supposed to just make more of everything. So, if AI works as advertised, then you'd probably expect a brief period of highly increased profit margins (by the consumers of AI) followed by rapid _deflation_ as the value of everyone's dollar increases exponentially. Of course, neither of those things is going to happen, because the AI sales pitch is actually a pyramid scheme, so you get the people at the top raking in cash, while everyone else tries to sucker the next tier of buyers so that they can make their buck.
I think the problem is moreso that making useful things for enterprise with AI right now is actually pretty hard because context and attention management is hard, the token cost for complex tasks scales fast, and model's lack of intuition for fuzzy decision-making.
There are hordes of grifters promising things they can't deliver and reaping in millions in capital from investors who are equally confused about the challenges of designing useful AI.
That said, AI can do useful things when properly designed. The market finding the people who can make this happen won't happen as fast as people expect.
Came here to say this. What AI is doing with math is essentially fuzzing, but looking for valid inputs that solve a problem and the inputs are mathematical abstractions. It's a cool approach, but AI doesn't understand what's going on, and without understanding it won't be able to create the next generation of mathematical abstractions needed for the next generation of proofs.
I don't think that's true. If what you're doing is building a fuzzer for mathematical proofs then just say that? The fact that it's doing some of the initial work on hard problems is cool. So is the fact that the promise of that new approach is having a social effect of crowd sourcing talented people to follow up on that work. No need to try to misrepresent it as more than that.
This technology has surpassed the the world's best mathematicians at the (explicitly and openly stated) goal by which they measure and reward mathematical progress. Such an advancement that it seems to have thrown the entire field into existential self-doubt. And then someone sits at their keyboard and says it is just a fuzzer.
You seem to be misunderstanding the premise of the statement. Go write, "print 'foo';" and copy and paste that statement one hundred thousand times. Congratulations, you just wrote one hundred thousand lines of functioning code! Was that hard? No? Okay, so how is this different from other code? The difference is that it's easy to _understand_ how that code works, because it's the same behavior repeated over and over. So, writing code is easy, but understanding code is difficult! And, when we code with AI, undertanding is precisely the part that it can't handle, even though that's where almost all of the value is!
Personally, I would tell you that whatever understanding you gain may still have bugs. Unless your understanding is as complete as a formal treatment of the code, then there may still be bugs in the code due to shared misunderstandings between author and reviewer. The biggest one is both having an incomplete understanding of what a library function does.
So while there may be some overlap, particularly if each person has full understanding of the code's dependencies, in the general case, understanding code and finding bugs are quite different aims.
If, by your definition of understanding, you can understand something without knowing how it works, then what would be the point in understanding it?
Your argument underscores the fact that understanding exists on a spectrum and that deep understanding can be difficult, or even impossible to achieve. Even formal verification seeks to verify certain properties of a system, and doesn't represent anything close to comprehensive understanding, and the process of formal verification is also guided by a fallible human. In a lot of ways, formal verification is just pushing up to review of a different "programming language."
So, good review is really hard, but ignoring the difficulty doesn't make it go away.
You’re confusing the difference between understanding and comprehending. The former is partial but useful within a context, the latter is total and is the result of mastery. One may understand an abstracted interface and how it works from the perspective of what it does in relation to solving a domain problem, but that doesn’t require them to know how it works at the level of any function/procedure’s mechanism.
While it may be true that formal verification doesn’t yield comprehensive understanding of code in certain forms, in a way it does by ensuring the code is only able to perform up to isomorphism with what the domain requires. Further understanding of how it accomplishes that is meaningless due to abstraction. But there are a number of techniques of formal methods that do require comprehensive understanding to be taken as valid, such as the structured proofs Dijkstra was famous for promoting. Also the classic example of Temporal Logic specs don’t compose, so the specifier must design the spec from scratch basically every time. Even using Hoare logic would require one to verify every line and all functions that are called for the purpose of solving a particular problem because of the difficulty of formally describing a function’s behavior in total.
So while I understand where you’re coming from, I do think that for any meaningful understanding regarding code, formal verification will provide it to the verifier. That is, as much as may reasonably be understood from the code is learned during any formal verification process.
This is largely my take as well. When I review code, I am checking for correctness. If I find something is not correct, that's a bug (or a bug waiting to happen). If I can't understand whether or not something is correct, that's a problem. If I don't know what the correct behavior should be, that's a problem.
Though I do think there is value in the original post. Re-framing is a powerful creative tool when you hit a mental dead end. And the responses let people share the other benefits that change management can bring.
I think you just made some strong arguments for classifying them as gatekeepers. The idea, like you said, is to make it so that competitors can enter the market and pick up the slack in areas where AWS and Azure are dropping the ball.
reply