411–420 of 448 posts
Earlier quoted context omitted.
When you go to write a line of code, how do you decide what to write?
> When you go to write a line of code, how do you decide what to write? depends ofcourse, what am i writing for ? a feature, a bugfix, refactor ... ?
> rather than having humans review AI-generated code, I’d much rather have the AI prove to me that the code it has generated is correct. If it can do that, I’ll take AI-generated code over handcrafted code (with all its artisanal bugs) any day! I wouldn't. An unreadable mess that has been formally verified is worse than a clear easy to understand piece of code that has not. Code is rarely written from scratch. As lon…
You already have this problem whenever you are using a library in any programming language. Unless you are extremely strict, vendor it and read line by line what the library does, you are just trusting that the code that you are using works. And nothing is stopping the AI from making the unreadable mess more readable in later iterations. It can make it pass the spec first and make it cleaner later. Just like we do!
Earlier quoted context omitted.
In practice it would be encoded in comments, automated tests and docs, with varying levels of success. It’s actually similar to tests in a way: they provide additional confidence in the code, but at the same time ossify it and make some changes potentially more difficult. Interestingly, they also make some changes easier, as long as not too many types/tests have to be adapted.
This reads to me like an argument for better refactoring tools, not necessarily for looser type systems. Those tools could range from mass editing tools, IDEs changing signatures in definitions when changing the callers and vice versa, to compiler modes where the language rules are relaxed.
The funny part of “AI will make formal verification go mainstream” is that it skips over the one step the industry still refuses to do: decide what the software is supposed to do in the first place. We already have a ton of orgs that can’t keep a test suite green or write an honest invariant in a code comment, but somehow we’re going to get them to agree on a precise spec in TLA+/Dafny/Lean and treat it as a blocking…
Earlier quoted context omitted.
I'm not sure how a "spec with floats" differs from a spec with networks, RAM, 64-bit integers, multi-level cache, or any computing concept, none of which exists as a primitive in mathematics. A floating point number is a pair of integers, or sometimes we think about it as a real number plus some error, and TLAPS can check theorems about specifications that describe floating-point operations. Of course, things can bec…
Those things, unlike floats, have approximable-enough facsimiles that you can verify instead. No tools support even fixed point decimals. This has burned me before when I e.g needed to take the mean of a sequence.
The complications in describing machine-representable numbers also apply to integers, but these complications can be important, and the level of detail matters just as it matters when representing RAM or any other computing concept. Unlike, say, strings, there is no single "natural" mathematical representation of floating point numbers, just as there isn't one for software integers (integers work differently in C, Java, JS, and Zig; in some situations you may wish to ignore these differences, in others - not). You may want to think about floating point numbers as a real + error, or you may want to think about them as a mantissa-exponent pair, perhaps with overflow or perhaps without. The "right" representation of a floating point number highly depends on the properties you wish to examine, just like any other computing construct. These complications are essential, and they exist, pretty much in the same form, in other languages for formal mathematics.
Is there a difference here between a proof and an automated test? I'm curious what a proof would look like compared to my RSpec unit tests and what the actual implementation would look like.
A test tests some - but not all - of the paths through your code. And some - but not all - of the inputs you might see. A proof establishes that your code works correctly on all paths, inputs, etc.
You could still have written the model wrong, you could still have not accounted for something important in your constraints. But at least it will give you a definite answer to “Does this model do what you say it does?”.
Then there are cases when an exhaustive search of the entire state space is not possible and best you can do is a stochastic search within it and hope that “Given a random sampling of all possible inputs, this model has respected the constraints for T amount of time, we can say with 99.99999998% certainty that the model follows the constraints”.
I've been toying with vibecoding rust - hardly formal verification, but it is a step closer than python that's for sure. So far so good, though the smaller amount of training data is noticeable.
vibecoding rust sounds cool, which model are you using? I have tried in the past with GPT4o and Sonnet 4, but they were so bad I thought I should just wait a few years.
Earlier quoted context omitted.
I agree. I think we've gotta get through the rough couple of "AI slop" years of code and we'll come out of it the other side with some incredible tools. The reason we don't all write code to the level that can operate the Space Shuttle is because we don't have the resources and the projects most of us work on all allow some wiggle room for bugs since lives generally aren't at risk. But we'd all love to check in code…
at some level it's not really an engineering issue. "bug free" requires that there is some external known goal with sufficient fidelity that it can classify all behaviors as "bug" or "not bug". This really doesn't exist in the vast majority of software projects. It is of course occasionally true that programmers are writing code that explicitly doesn't meet one of the requirements they were given, but most of the tim…
What if the AI kept bringing up unspecified cases and all you (the human) had to do all day was respond to it on what the behavior should be in each case? In this model the AI would not specify the outcomes; the specification is whatever you initially specified, and your responses to the AI's questions about the outcomes. At some point you'd decide that you'd answered enough questions (or the AI could not come up with any more unspecified cases), and bugs would be in what remained, but it would still mean substantially more thinking about cases than now.
Earlier quoted context omitted.
I disagree. Right now, feedback on correctness is a major practical limitation on the usefulness of AI coding agents. They can fix compile errors on their own, they can _sometimes_ fix test errors on their own, but fixing functionality / architecture errors takes human intervention. Formal verification basically turns (a subset of) functionality errors into compile errors, making the feedback loop much stronger. "Com…
I completely agree it's appealing, I just don't see a reason to assume that an agent will be able to succeed at it and at the same time fail at other things that could make the whole exercise redundant. In other words, I also want agents to be able to consistently prove software correct, but if they're actually able to accomplish that, then they could just as likely be able to do everything else in the production of…
But that is much simpler to understand: eventually finding a proof using guided search (machines searching for proofs, multiple inference attempts) takes more effort than verifying a proof. Formal verification does not disappear, because communicating a valuable succinct proof is much cheaper than having to search for the proof anew. The proofs will become inevitable lingua franca (like it is among capable humans) for computers as well. Basic economics will result in adoption of formal verification.
Whenever humans found an original proof, their notes will contain a lot of deductions that were ultimately not used, they were searching for a proof, using intuition gained in reading and finding proofs of other theorems. It's just that LLM's are similarily gaining intuition, and at some point become better than humans at finding proofs. It is currently already much better than the average human at finding proofs. The question is how long it takes until it gets better than any human being at finding proofs.
The future you see where the whole proving exercise (if by humans or by LLMs) becomes redundant because it immediately emits the right code is nonsensical: the frontier of what LLM's are capable of will move gradually, so for each generation of LLMs. there will always be problems it can not instantly generate provably correct software (but omitting the according-to-you-unnecessary proof). That doesn't mean they can't find the proofs, just that it would have to search by reasoning, with no guarantee if it ever finds a proof.
That search heuristic is Las Vegas, not Monte Carlo.
Companies will compare the levelized operating costs of different LLM's to decide which LLMs to use in the future on hard proving tasks.
Satellite data centers will consume ever more resources in a combined space/logic race for cryptographic breakthroughs.
Earlier quoted context omitted.
> No one claims that good type systems prevent buggy software. That's exactly what languages with advanced type systems claim. To be more precise, they claim to eliminate entire classes of bugs. So they reduce bugs, they don't eliminate them completely.
No nulls, no nullability bombs. Forcing devs to pre-fix/avoid bugs before the compiler will allow the app means the programs are more correct as a group. Wrong, incomplete, insufficient, unhelpful, unimpressive, and dumb are all still very possible. But more correct than likely in looser systems.
I hate this meme. Null indicates something. If you disallow null that same state gets encoded in some other way. And if you don't properly check for that state you get the exact same class of bug. The desirable type system feature here is the ability to statically verify that such a check has occurred every time a variable is accessed.
Another example is bounds checking. Languages that stash the array length somewhere and verify against it on access eliminate yet another class of bug without introducing any programmer overhead (although there generally is some runtime overhead).