Formalizing CPython(broyojo.com)
41 pointsby carnevalem5 hours ago9 comments
  • jakobnissenan hour ago
    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.

  • eternauta3k39 minutes ago
    Is there a way to avoid the translation or replace it with normal parsing?
    • choeger30 minutes ago
      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.

  • senderista29 minutes ago
    Cite an AI-written document? Hell no.
  • bb88an hour ago
    Only 418?

    I would have expected around 10k.

    Edit: Professional python programmer.

  • woggy24 minutes ago
    Can we just develop in Lean and compile to something else for speed?
  • up2isomorphisman hour ago
    AI does not kill research, research kills pretty much itself already.
  • q4y2u35uk2 hours ago
    [flagged]
    • Ohentisan hour ago
      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.
    • perching_aixan hour ago
      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?

  • fny2 hours ago
    [flagged]
    • echelonan hour ago
      Stop using the word slop. It's a joke at this point.
      • creata17 minutes ago
        No offense, but that doesn't mean a whole lot coming from someone who's all in on the slop train, ArtCraft guy.
    • nurettin2 hours ago
      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".