5 ms·

I really look forward to the day AI-driven algorithm design + formal verification becomes the norm for performance critical computing. A programmer translates

I really look forward to the day AI-driven algorithm design + formal verification becomes the norm for performance critical computing. A programmer translates a natural-language spec into a machine-readable spec, feeds it to an AI-assisted compiler, and out pops an implementation that's more optimized than any human could ever hope to write, along with a lean proof of its correctness.

jplusequalt 4mo ago
>A programmer It won't be a programmer doing this work, because they will have gone the way of the dodo. It'll be workers specific to a certain domain (e.g. engineer, architect, accountant) doing this on top of their usual work. The software industry will collapse.
- CuriouslyC 4mo ago
  The architect/accountant won't be doing it either, they'll just be a liability lightning rod for people who are closer to devs than architects doing the actual day to day work. Sort of like a doctor will "manage" a team of nurse practitioners.
  - whattheheckheck 4mo ago
    Except medicine is 1000x older than software engineering as a field
xpct 4mo ago
I'm sure a system that could do this is economically optimal. Why are you looking forward to this, though?
- AndrewKemendo 4mo ago
  Not the OP but for me it’s: more optimized than any human could ever hope to write, along with a lean proof of its correctness.
kccqzy 4mo ago
You can look forward to that, but today I’m already experiencing something worse but close enough for all but the most critical code: AI-driven algorithm design + tests in your favorite property-based testing library (like OG QuickCheck in Haskell or hypothesis in Python). Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.
- pvillano 4mo ago
  Fully automated testing + revision loops are super cool and def something I want to play with And PBT is so close to language level invariants/preconditions/post-conditions that I dream of
whattheheckheck 4mo ago
How would you even be able to recognize the proof is valid? Or its own proof that it understands its own proof.... This ain't the future
- pvillano 4mo ago
  You don't need to check the proof. A regular proof is written to convince other mathematicians. A regular proof can skip details and contain mistakes. A formal proof cannot skip details or contain mistakes. A lean proof is a sequence of instructions that starts with a list of facts, and combines them into new facts until a target fact is produced. Each instruction in the sequence is one of a few allowed tactics provided by lean that always produce correct facts from correct facts. IF (1) you agree with the starting facts, (2) you are sure the target fact is what you're actually trying to prove and (3) the lean compiler says "yep, this is a valid sequence of instructions" THEN you can be sure the target fact is true. You can be sure the final fact is true, even if you don't understand all the steps, because it's written in lean, and lean only allows steps that are free from omissions or errors
  - whattheheckheck 4mo ago
    Have you actually written proofs in Lean with your professional reputation on the line?
dyauspitr 4mo ago
> A programmer translates a natural-language spec into a machine-readable spec Why do we need a human for this?
- pvillano 4mo ago
  Liability, and it's the hardest part.
xg15 4mo ago
...and no human will be able to understand the algorithm either.
- pvillano 4mo ago
  AlphaGo, through self-play, found new strategies to beat the best human players. But now that anyone can play against AlphaGo, humans are learning these strategies. Deepmind is saying people are learning from the algorithms AlphaEvolve is generating. They say the programs tend to be short. So maybe we will understand the algorithms

jplusequalt 4mo ago

>A programmer It won't be a programmer doing this work, because they will have gone the way of the dodo. It'll be workers specific to a certain domain (e.g. engineer, architect, accountant) doing this on top of their usual work. The software industry will collapse.

CuriouslyC 4mo ago
The architect/accountant won't be doing it either, they'll just be a liability lightning rod for people who are closer to devs than architects doing the actual day to day work. Sort of like a doctor will "manage" a team of nurse practitioners.
- whattheheckheck 4mo ago
  Except medicine is 1000x older than software engineering as a field

xpct 4mo ago

I'm sure a system that could do this is economically optimal. Why are you looking forward to this, though?

AndrewKemendo 4mo ago
Not the OP but for me it’s: more optimized than any human could ever hope to write, along with a lean proof of its correctness.

kccqzy 4mo ago

You can look forward to that, but today I’m already experiencing something worse but close enough for all but the most critical code: AI-driven algorithm design + tests in your favorite property-based testing library (like OG QuickCheck in Haskell or hypothesis in Python). Of course problems remain in both approaches: a human or AI needs to make sure the lean proof is proving the correct translation from natural language spec to a formal theorem, or the PBT is testing the right properties translated from natural language.

pvillano 4mo ago
Fully automated testing + revision loops are super cool and def something I want to play with And PBT is so close to language level invariants/preconditions/post-conditions that I dream of

whattheheckheck 4mo ago

How would you even be able to recognize the proof is valid? Or its own proof that it understands its own proof.... This ain't the future

pvillano 4mo ago
You don't need to check the proof. A regular proof is written to convince other mathematicians. A regular proof can skip details and contain mistakes. A formal proof cannot skip details or contain mistakes. A lean proof is a sequence of instructions that starts with a list of facts, and combines them into new facts until a target fact is produced. Each instruction in the sequence is one of a few allowed tactics provided by lean that always produce correct facts from correct facts. IF (1) you agree with the starting facts, (2) you are sure the target fact is what you're actually trying to prove and (3) the lean compiler says "yep, this is a valid sequence of instructions" THEN you can be sure the target fact is true. You can be sure the final fact is true, even if you don't understand all the steps, because it's written in lean, and lean only allows steps that are free from omissions or errors
- whattheheckheck 4mo ago
  Have you actually written proofs in Lean with your professional reputation on the line?

dyauspitr 4mo ago

> A programmer translates a natural-language spec into a machine-readable spec Why do we need a human for this?

pvillano 4mo ago
Liability, and it's the hardest part.

xg15 4mo ago

...and no human will be able to understand the algorithm either.

pvillano 4mo ago
AlphaGo, through self-play, found new strategies to beat the best human players. But now that anyone can play against AlphaGo, humans are learning these strategies. Deepmind is saying people are learning from the algorithms AlphaEvolve is generating. They say the programs tend to be short. So maybe we will understand the algorithms