{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreicpkaj2dee54vukr2nw43xlprvhmztrbkpowc3le46ttez2cwwlcy",
    "uri": "at://did:plc:pi6woz4d47bkuws673w2il2r/app.bsky.feed.post/3mhgpbo6427v2"
  },
  "path": "/t/the-fastest-way-to-feed-ghc-type-errors-to-llm/13827#post_9",
  "publishedAt": "2026-03-19T15:47:05.000Z",
  "site": "https://discourse.haskell.org",
  "tags": [
    "GitHub - jasisz/aver: Aver is a programming language for auditable AI-written code: verify in source, deploy with Rust, prove with Lean/Dafny · GitHub"
  ],
  "textContent": "I apologize in advance and this definitely doesn’t answer your question in regards to Haskell but I just wanted to point out this repo I found yesterday for a new AI specific language that builds LEAN proofs for each change. Seems to be exactly the type of thing that can keep these hallucination machines on a set of rigid guardrails: GitHub - jasisz/aver: Aver is a programming language for auditable AI-written code: verify in source, deploy with Rust, prove with Lean/Dafny · GitHub\n\nSeems like the absolute best way to truly get the most out of each token in the LLM.\n\nSince it builds Rust, perhaps it could also build Haskell Core? Anyway, it’s an interesting concept that materializes some of the theories about best practices that I’ve pondered upon noticing how much better LLM’s are when they have a rich type system like Haskell’s for feedback.",
  "title": "The fastest way to feed ghc type errors to LLM"
}