Formalizing CPython

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.

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.

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"?).

Only 418?

I would have expected around 10k.

Edit: Professional python programmer.

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

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?

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

[flagged]

[flagged]

Cite an AI-written document? Hell no.

[flagged]

[flagged]

[flagged]