A verified proof guarantees the code is correct, but does it guarantee what you actually meant to guarantee? claimcheck uses round-trip informalization to narrow the gap between formal proof and original intent.
  • MadhuGururajan@programming.devEnglish
    1·
    9 days ago

    it is quite terrifying that people think translating from formal constraints in math to informal english is either accurate or deterministic.

    And they ask the LLM to not look at requirements but who is guaranteeing it won’t just hallucinate them out of thin air later when messy prompts inevitably trigger a butterfly effect?