Wouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
One advantage of this approach is that it can be done both on the C implementation code and the Python standard library. It's a bit approximate -- automatic retrofitting of formal specification maybe it helps to think of it as a stepping stone for simple automated testing and property based testing.
I think this approach to bug hunting is super promising (obviously - it finds a ton of bugs). The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. The approach taken by these people, the same approach as when the Julia folks did it, isn't really automatable, because it requires a lot of both human and AI agent work.
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
I don’t think Lean can get you dynamic, high performance generic code, so you can’t really replace Julia with Lean.
But I get, and agree with, your observation that AI encourages better static tooling, which Julia does not have, and that it would be a good idea to have a language that has both good static tooling, and which is fit for iterative exploration and experimentation. And that this parallels the two language problem.
You can writer solvers for bits of code and make them part of your test runs, I do that for gnarly bits, especially gnarly bits written by AI where the drift would not be obvious to me.
I read it. It explained the formalization effort in simple terms without too much jargon.
I actually found it quite informative about how formalization can go bad -- assuming memory allocation always succeeds, memory allocation will never reuse the same address, the user won't subclass exceptions, etc.
I often “oh, this is going to be an interesting article written by someone about how they use an LLM to do X” and then start and discover that the person wrote the article via prompting. I guess if you think LLMs are amazing and that you’ve gotten into a rhythm of offloading all the labour to them, you see writing your own posts as a waste of time. I just wish those posts came with disclaimers telling the reader that reading it is a waste of time too and the reader should just point an agent at it or whatever.
That reminds me of what you see in some Issues on AI-related GitHub repos. A 'conversation' where people are just pasting big walls of text with way too much formatting back and forth to each other.
Isn't the Lean programming language a pure functional programming language? But surely much of the CPython C code is not written in a pure functional style. So the translation must not be trivial. How do they do it?
In their example, the CPython function get_len_of_range is a pure function, and the translation is trivial, as expected.
It would be helpful to show us a CPython function which is not purely functional, and its (presumably less trivial) translation.
I see they don't have complete coverage yet. Did they cherry-pick the functional parts of CPython to get started?
"C and Python versions disagree" and "other" is really due to fuzzing, not to proofs. And those sections are more than half of the total number of bugs found.
Probably most of the rest is fuzzing, too, with Lean and unspecified "proofs" thrown in to sound magical.
The way I understand it, the two implementations can only differ in the result if the lean translation was done incorrectly; that's the point, you don't want to use those to prove invariants in the next step.
For the next step, I have the same question. It's the crux of the approach and the article is surprisingly light on detail:
> The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something
So it was done by AI but they don't make entirely clear how the interesting proof statements were chosen.
yes, one can say it is "guessing" but taking in these into account:
> Source, in order of preference: (a) the implementation disagreeing with itself (C vs Python twin, fast vs slow path, method vs equivalent method, round-trips, str vs bytes); (b) undisputed invariants (no crash, no internal error leaking, results in range, no hang); (c) explicit doc sentences read in context.[...]
They describe it later. Essentially, they are asking the AI for each function to give them a property that basically means "this function is correct", and then they let it prove that property.
I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.
it's a matter of how much of a modeling gap do you choose to accept.
for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.
just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.
Because in order for the proof to succeed, Lean needs "strange" assumptions about the code. This rare assumptions are the conditions to trigger the bug.
Imagine a proof that needs the axiom that all numbers are below 2^32. What happens if my system is expected to handle numbers greater than 2^32?? There you have the bug... Also it could mean that the system is not validating the boundness of the input, and 2^32 is the maximum that allows for coherent execution downstream of the execution. In both cases, it needs to be checked :)
formal modeling and verification doesn't become 100% magically useless just because you can't assert semantic correspondence automatically. one would expect a champion of understanding to understand this.
way to take issue with credibility from a blatant sockpuppet account by the way. like, really dude?
It's not a snarky sting. I think ArtCraft is very impressive, to be clear. I just couldn't figure out another concise way to provide the relevant context that would be needed to understand my comment.
Now if I did want to be snarky, this is the part where I'd point to the "assume good faith" part of the guidelines.
We can only judge the way the words land when they appear on the page. We can’t assume what you were thinking and discern that you may have intended to convey something different. People often underestimate how mean their words seem when read by others. Nobody likes to think of themselves in negative terms. Almost everyone means well. I’m sure you do.
But the guidelines are clear about snark, swipes, and calling names. They are also clear about conversing curiously and being thoughtful and kind. Please just try harder to figure out ways of expressing your thoughts kindly.
It's not name-calling to call the guy who created the ArtCraft suite... the guy who created the ArtCraft suite. And it's not a "swipe" to point out that someone who uses AI assistance to such an extent would have a very different view of the word "slop" than someone who doesn't, and so that they might not be a great judge of whether the word "slop" is seen as a "joke".
Calling others' viewpoints "jokes" is pretty damn abrasive, by the way. Quite a bit less kind than anything I've said here, in my humble view. But you're entitled to your view, obviously.
It's not an ad hominem if it actually explains why their opinion should not be presented as a universal statement, or something that others should police their language by (recalling that the comment began with the command "Stop using the word slop."). I think that's pretty obvious.
> calling anything with genai involvement slop, irrespective of their actual quality, is not intentionally negatively generalizing?
I guess, in the sense that all hyperbolic language can be interpreted as negative generalization? That doesn't mean hyperbolic language is useless.
> It's not an ad hominem if it actually explains why their opinion should not be presented as a universal statement, or something that others should police their language by
which it didn't
so "insult" is still on the table btw? wasn't mixing the two, that was a genuine "or" operation there.
> I guess, in the sense that all hyperbolic language can be negative generalization
no, in the sense that you're laundering in your normative stance about the subject into the language you use, robbing other people of the ability to articulate themselves as normal.
meaning might be associated to words within a person, but language works by consensus. they have (at minimum!) every right to bemoan your usage of slop as you do spreading it.
explicit manipulation of others' language not okay, implicit manipulation of others' language is okay?
Right, because "bemoaning" the usage of a word is the same as commanding other people to stop using it, calling it a "joke" with no further elaboration. That's totally the kind, thoughtful way to go about that.
Look, how about we both stop filling up this thread with pointless junk? If you want, we can say you won, and you get the internet points, or you've exposed me as the evil bad faith actor trying to get away with a mean comment, or whatever the point of this was.
> That's totally the kind, thoughtful way to go about that.
it isn't; i generally super don't appreciate calls for action. so if you wanted to believe i came to defend it, that was a swing and a miss.
> If you want, we can say you won, and you get the internet points, or you've exposed me as the evil bad faith actor trying to get away with a mean comment, or whatever the point of this was.
sure! will fit in just right when you'll later retell this story from the pov of an innocent victim who dindunuttin at all.
or we could be a bit more honest, and address why we're of the position that we're approaching from, genuinely without trying to taunt the other. would almost resemble an adult conversation. but then i'd be lying if i said i care or have any interest in doing so at this point, and i'd be equally surprised if you do.
so maybe wrapping it up here really is the way to go, after all.
Please don't post like this on HN. Your comments in this subthread are also snarky and escalatory, and that's not okay, no matter who or what position you're supporting or defending.
My role here is to uphold the guidelines, which includes pointing it out to people that they have acted outside the guidelines when they may not realize that they’ve done so. Nobody said or thought you were an “evil bad faith actor”. It was a polite ask to try harder, which we do all the time. The ongoing escalation doesn’t make you seem like you’re committed to raising the standards here. This place only exists because enough people make the effort to push the standards up. It’s up to you what you want your role to be.
dude u so biased we can all see it. Link me to all the times you "moderated" the Pro Slop bros for telling a skeptic they're "coping", "left behind" etc?
But you and dang are working overtime to protect altman and his minions from having their feelings hurt or be made of fun of.
We post moderation comments to people on all sides of all topics all the time. We're more proactive than just about any other site in filtering out LLM-generated comments, and we downweight or discard low-quality AI-generated posts and projects many times daily. Our inbox is flooded with them, and it's a huge time-suck for us to deal with them all. It makes no difference to the people at the AI companies and their executives whether people on HN say mean things about them. It does make a difference to fellow community members who are trying to participate earnestly and figure out how to make the best of the challenges we are all facing. We're not primarily concerned with people being jerks towards LLM companies or their executives. We're concerned about people being jerks to each other on HN, no matter what it's about.
Wouldn't it be more productive spending the tokens on adding ACSL annotations to verify CPython with Frama-C? You'd verify the actual runtime instead of an AI translation of it, and fixes could be contributed upstream directly.
One advantage of this approach is that it can be done both on the C implementation code and the Python standard library. It's a bit approximate -- automatic retrofitting of formal specification maybe it helps to think of it as a stepping stone for simple automated testing and property based testing.
Same approach for Julias stdlib: https://discourse.julialang.org/t/formalizing-julia-in-lean-...
Interesting also the prompt of the python formalization (and the blog post) mentions the julia-in-lean:
https://github.com/Broyojo/python-formalization/blob/main/AG...
I think this approach to bug hunting is super promising (obviously - it finds a ton of bugs). The long-term problem is how this kind of bug-hunting can be done routinely, e.g. as part of a test suite. The approach taken by these people, the same approach as when the Julia folks did it, isn't really automatable, because it requires a lot of both human and AI agent work.
I guess longer term it needs to be built into the language, to prevent code and lean proofs from drifting. I.e. it could be opt-in properties that are written along the code, and which is then checked in the test suite. So very similar to ordinary compiler checks, except more expressive and expensive, and done only at test time.
At that point you might as well use Lean?
It would solve the two language problem :-)
I don’t think Lean can get you dynamic, high performance generic code, so you can’t really replace Julia with Lean.
But I get, and agree with, your observation that AI encourages better static tooling, which Julia does not have, and that it would be a good idea to have a language that has both good static tooling, and which is fit for iterative exploration and experimentation. And that this parallels the two language problem.
yep
bend programming language already solved this problem: https://bend-lang.com/
You can writer solvers for bits of code and make them part of your test runs, I do that for gnarly bits, especially gnarly bits written by AI where the drift would not be obvious to me.
Interesting. Now I have an idea to extend my tooling flow, thanks.
Does anyone read articles written by AI? This is a serious question.
I read it. It explained the formalization effort in simple terms without too much jargon.
I actually found it quite informative about how formalization can go bad -- assuming memory allocation always succeeds, memory allocation will never reuse the same address, the user won't subclass exceptions, etc.
Next generation AI when they eventually get in the corps?
Does anyone use code written by AI? Just as serious question.
Because I honestly can't understand how we celebrate being pushed into not writing code, but get grumpy about everything else.
I often “oh, this is going to be an interesting article written by someone about how they use an LLM to do X” and then start and discover that the person wrote the article via prompting. I guess if you think LLMs are amazing and that you’ve gotten into a rhythm of offloading all the labour to them, you see writing your own posts as a waste of time. I just wish those posts came with disclaimers telling the reader that reading it is a waste of time too and the reader should just point an agent at it or whatever.
I start from the assumption that anything written coming from AI enthusiasts is also written by AI and skip it by default.
That reminds me of what you see in some Issues on AI-related GitHub repos. A 'conversation' where people are just pasting big walls of text with way too much formatting back and forth to each other.
I think AI output is like your own farts. We all smell our own but others don't want to be subject to it.
Isn't the Lean programming language a pure functional programming language? But surely much of the CPython C code is not written in a pure functional style. So the translation must not be trivial. How do they do it?
In their example, the CPython function get_len_of_range is a pure function, and the translation is trivial, as expected.
It would be helpful to show us a CPython function which is not purely functional, and its (presumably less trivial) translation.
I see they don't have complete coverage yet. Did they cherry-pick the functional parts of CPython to get started?
Only 418?
I would have expected around 10k.
Edit: Professional python programmer.
they don't have full coverage yet
"C and Python versions disagree" and "other" is really due to fuzzing, not to proofs. And those sections are more than half of the total number of bugs found.
Probably most of the rest is fuzzing, too, with Lean and unspecified "proofs" thrown in to sound magical.
I'm confused about a few points, would love it if someone could help clear it up!
- if the rewrite in Lean happens line-by-line, how can the two implementations differ in their result (Step 2)?
- how does this approach know "something that should always be true" in Step 3 (is it the intelligence of the LLM "guessing"?).
The way I understand it, the two implementations can only differ in the result if the lean translation was done incorrectly; that's the point, you don't want to use those to prove invariants in the next step.
For the next step, I have the same question. It's the crux of the approach and the article is surprisingly light on detail:
> The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something
So it was done by AI but they don't make entirely clear how the interesting proof statements were chosen.
yes, one can say it is "guessing" but taking in these into account:
> Source, in order of preference: (a) the implementation disagreeing with itself (C vs Python twin, fast vs slow path, method vs equivalent method, round-trips, str vs bytes); (b) undisputed invariants (no crash, no internal error leaking, results in range, no hang); (c) explicit doc sentences read in context.[...]
https://github.com/Broyojo/python-formalization/blob/main/AG...
They describe it later. Essentially, they are asking the AI for each function to give them a property that basically means "this function is correct", and then they let it prove that property.
Is there a way to avoid the translation or replace it with normal parsing?
In principle, yes.
I am not a lean expert, but I imagine that python primitives like dicts, ints, functions, etc., have been defined in lean. So if you add a way to annotate python code with a proof, you should as well be able to automatically translate it to Lean completely.
it's a matter of how much of a modeling gap do you choose to accept.
for full, honest to god, end to end verification this would be insufficient. but you don't need that in order to reap benefits.
just gotta make sure you actually bound the triage process with some sort of automated verification process. like comparative test cases or similar. otherwise it's just a particularly expensive way of agentic hallucination.
Stupid question: if the lean4 code is a copy of the C code, how does "it" know which code is a bug and which code is working as intended?
Because in order for the proof to succeed, Lean needs "strange" assumptions about the code. This rare assumptions are the conditions to trigger the bug.
Imagine a proof that needs the axiom that all numbers are below 2^32. What happens if my system is expected to handle numbers greater than 2^32?? There you have the bug... Also it could mean that the system is not validating the boundness of the input, and 2^32 is the maximum that allows for coherent execution downstream of the execution. In both cases, it needs to be checked :)
Can we just develop in Lean and compile to something else for speed?
Lean is actually pretty speedy as is, and it enables much harder optimizations[1]
[1] https://github.com/kim-em/lean-zip#verification-enables-perf...
Of course.
[flagged]
[flagged]
Cite an AI-written document? Hell no.
[flagged]
Some parts of this are true, but bringing up z3 is kind of a random tangent without any actual knowledge to be shared behind it.
formal modeling and verification doesn't become 100% magically useless just because you can't assert semantic correspondence automatically. one would expect a champion of understanding to understand this.
way to take issue with credibility from a blatant sockpuppet account by the way. like, really dude?
[flagged]
[flagged]
Stop using the word slop. It's a joke at this point.
No offense, but that doesn't mean a whole lot coming from someone who's all in on the slop train, ArtCraft guy.
> ArtCraft guy.
Please don’t post comments with snarky stings in the tail on HN. Disagreement is fine. Personal swipes are definitely not.
https://news.ycombinator.com/newsguidelines.html
It's not a snarky sting. I think ArtCraft is very impressive, to be clear. I just couldn't figure out another concise way to provide the relevant context that would be needed to understand my comment.
Now if I did want to be snarky, this is the part where I'd point to the "assume good faith" part of the guidelines.
We can only judge the way the words land when they appear on the page. We can’t assume what you were thinking and discern that you may have intended to convey something different. People often underestimate how mean their words seem when read by others. Nobody likes to think of themselves in negative terms. Almost everyone means well. I’m sure you do.
But the guidelines are clear about snark, swipes, and calling names. They are also clear about conversing curiously and being thoughtful and kind. Please just try harder to figure out ways of expressing your thoughts kindly.
It's not name-calling to call the guy who created the ArtCraft suite... the guy who created the ArtCraft suite. And it's not a "swipe" to point out that someone who uses AI assistance to such an extent would have a very different view of the word "slop" than someone who doesn't, and so that they might not be a great judge of whether the word "slop" is seen as a "joke".
Calling others' viewpoints "jokes" is pretty damn abrasive, by the way. Quite a bit less kind than anything I've said here, in my humble view. But you're entitled to your view, obviously.
> that doesn't mean a whole lot coming from someone who's all in on the slop train
so this was not meant to be an insult / ad hom?
calling anything with genai involvement slop, irrespective of their actual quality, is not intentionally negatively generalizing?
i'm not sure who are you trying to convince.
> so this was not meant to be an insult / ad hom?
It's not an ad hominem if it actually explains why their opinion should not be presented as a universal statement, or something that others should police their language by (recalling that the comment began with the command "Stop using the word slop."). I think that's pretty obvious.
> calling anything with genai involvement slop, irrespective of their actual quality, is not intentionally negatively generalizing?
I guess, in the sense that all hyperbolic language can be interpreted as negative generalization? That doesn't mean hyperbolic language is useless.
> It's not an ad hominem if it actually explains why their opinion should not be presented as a universal statement, or something that others should police their language by
which it didn't
so "insult" is still on the table btw? wasn't mixing the two, that was a genuine "or" operation there.
> I guess, in the sense that all hyperbolic language can be negative generalization
no, in the sense that you're laundering in your normative stance about the subject into the language you use, robbing other people of the ability to articulate themselves as normal.
meaning might be associated to words within a person, but language works by consensus. they have (at minimum!) every right to bemoan your usage of slop as you do spreading it.
explicit manipulation of others' language not okay, implicit manipulation of others' language is okay?
> That doesn't mean hyperbolic words are useless.
right, that they are not. great?
Right, because "bemoaning" the usage of a word is the same as commanding other people to stop using it, calling it a "joke" with no further elaboration. That's totally the kind, thoughtful way to go about that.
Look, how about we both stop filling up this thread with pointless junk? If you want, we can say you won, and you get the internet points, or you've exposed me as the evil bad faith actor trying to get away with a mean comment, or whatever the point of this was.
> That's totally the kind, thoughtful way to go about that.
it isn't; i generally super don't appreciate calls for action. so if you wanted to believe i came to defend it, that was a swing and a miss.
> If you want, we can say you won, and you get the internet points, or you've exposed me as the evil bad faith actor trying to get away with a mean comment, or whatever the point of this was.
sure! will fit in just right when you'll later retell this story from the pov of an innocent victim who dindunuttin at all.
or we could be a bit more honest, and address why we're of the position that we're approaching from, genuinely without trying to taunt the other. would almost resemble an adult conversation. but then i'd be lying if i said i care or have any interest in doing so at this point, and i'd be equally surprised if you do.
so maybe wrapping it up here really is the way to go, after all.
Please don't post like this on HN. Your comments in this subthread are also snarky and escalatory, and that's not okay, no matter who or what position you're supporting or defending.
[flagged]
Both of you need to stop.
My role here is to uphold the guidelines, which includes pointing it out to people that they have acted outside the guidelines when they may not realize that they’ve done so. Nobody said or thought you were an “evil bad faith actor”. It was a polite ask to try harder, which we do all the time. The ongoing escalation doesn’t make you seem like you’re committed to raising the standards here. This place only exists because enough people make the effort to push the standards up. It’s up to you what you want your role to be.
[dead]
[flagged]
dude u so biased we can all see it. Link me to all the times you "moderated" the Pro Slop bros for telling a skeptic they're "coping", "left behind" etc?
But you and dang are working overtime to protect altman and his minions from having their feelings hurt or be made of fun of.
slop
We post moderation comments to people on all sides of all topics all the time. We're more proactive than just about any other site in filtering out LLM-generated comments, and we downweight or discard low-quality AI-generated posts and projects many times daily. Our inbox is flooded with them, and it's a huge time-suck for us to deal with them all. It makes no difference to the people at the AI companies and their executives whether people on HN say mean things about them. It does make a difference to fellow community members who are trying to participate earnestly and figure out how to make the best of the challenges we are all facing. We're not primarily concerned with people being jerks towards LLM companies or their executives. We're concerned about people being jerks to each other on HN, no matter what it's about.
Title says formalizing, article amounts to "we asked claude to check one result with lean, got bad results, then we told it to make no mistakes".