Formalizing CPython

Same approach for Julias stdlib: https://discourse.julialang.org/t/formalizing-julia-in-lean-...

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.

Does anyone read articles written by AI? This is a serious question.

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?

Is there a way to avoid the translation or replace it with normal parsing?

Only 418?

I would have expected around 10k.

Edit: Professional python programmer.

Cite an AI-written document? Hell no.

Can we just develop in Lean and compile to something else for speed?

[flagged]

[flagged]

Lean can check Lean code, not arbitrary code. There's no telling what gets lost in translation. There's other formal verification systems out there like Z3 which live alongside the code and can verify the actual implementation. There's so much hype around Lean but few people actually understand it. But hey who needs to understand anything anymore? We have vibe coding!

And whole article consists of blatantly Claude-generated text. Way to throw credibility out the window.

[flagged]

[flagged]