undefined

points

[-]

The issue with formal proofs is that we might end up with correct code that does the wrong thing. I mean, something that the market doesn't care about. At the same time a buggy set of PHP scripts does what people care about and captures the market. Think about 20+ years ago and you find a lot of examples.

by psd111 hours ago|

parent|

[-]

https://xkcd.com/224/ lol

Zuckerberg became rich on php, which grinds my gears almost as much as the genocide thing.

In fairness, my peers at $corp used to ship while I was sad-Wojciech "no you can't create tech debt". The universe is cruel to people who care.

by frumplestlatz9 hours ago|

parent|

prev|

[-]

Well, sure — and the issue with tests is we might end up with well-tested code that does the wrong thing.

by frumplestlatz9 hours ago|

prev|

[-]

That's literally the opposite of reality; the research and adoption have consistently produced code of extremely high quality, at great cost.

The problem has always been:

- It's extremely labour-intensive, and even small changes to the code can require an enormous amount of new proof work.

- The skills required to formally verify software are very different from the skills required to write it, and the set of people capable of doing so is much smaller.

- Code has to be written with verification in mind, against a specification that expresses invariants that can actually be verified, and that is coherent enough that you can derive useful high-level properties of the system from it.

You needed two teams — verification and development. Verification would always be behind the development team, while also having to feed requirements and design changes back to the developers. Everything slowed to a crawl.

AI changes this. A coherent, verifiable, useful specification isn't easy to write — but it's far easier to write than the software itself, and AI can do most of that work: both drafting the spec and proving that it's consistent and that the high-level properties you actually care about follow from it.

More importantly, a high-level spec is far easier to read and reason about than the reams of code required to actually implement something. Which means:

- AI does the grunt work of writing and proving the spec; humans only have to carefully review that high-level artifact.

- AI writes code it must also prove conforms to the spec, so humans can be assured it's correct without babysitting the AI.

- Changes are driven top-down: evolve the spec first, then have the AI fix the implementation and re-prove conformance.

Our (very, very large) company is rapidly going all-in on formal verification across projects we never would have dreamed of verifying before; the velocity hit and the man-hour cost were only worth paying for truly critical infrastructure.

by doug_durham3 hours ago|

parent|

[-]

I’m sure in certain domains this makes sense. However, English is a poor language for doing reasoning in. More and more I’m relying on the code itself as the documentation. One of the superpowers of LLMs is reading code. and turning it into readable English. I don’t keep the English prose around. I delete it. In your example, I don’t see having two sets of artifacts. I see working with an LLM to generate a code base, which is the specification. You still need to have sets of requirements that list the invariants and other parameters. But the process becomes generating the code, and then having the LLM read the code to see if it meets the requirements and invariants.

by em-bee18 hours ago|

prev|

[-]

what i expect to change with LLMs is the benefit you get from automated testing. which is really what LLMs need. tools that tell you something is wrong may not speed up a human developer, but they will allow LLMs to make corrections by itself until the warnings go away. so while it may not be worth it to a human developer, it may well be worth it for an LLM.