{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreifvpkbdjq46va5mgvhug5uisxl54jwfnd2vhukoumn55jlqdljfrq",
    "uri": "at://did:plc:zyvv64s26uy7h2rwhhdq5e5f/app.bsky.feed.post/3mgaitiv6zys2"
  },
  "path": "/2026/03/04/proofs/",
  "publishedAt": "2026-03-04T05:00:00.000Z",
  "site": "https://inkdroid.org",
  "tags": [
    "marc",
    "rust",
    "engineering",
    "proves",
    "This",
    "Dan Chudnov",
    "mrrc",
    "pymarc",
    "not alone"
  ],
  "textContent": "This is a good post from Dan Chudnov about his work on mrrc (a Python wrapped Rust library for MARC data) and how agentic-coding tools (e.g. Claude Code) can be useful for learning, adding rigor and engineering that might otherwise not be practical or feasible.\n\npymarc has been proven through years of use, bug reporting, and improvements, but has never been formally verified, or had that level of rigorous attention. I remain skeptical about building AI into everything, but Dan has helped me see a silver lining where, as code gets easier to write, with all its potential for slop, it also simultaneously opens a door to helping making it more reliable and performant.\n\nAnd, Dan is not alone in thinking this. What if the tools for describing how software _should_ work, and for measuring how software _does_ work, get much, much better? If formal verification tools become more accessible and can be applied not just at the base layer of systems (where it really matters) but in middle and frontend layers of applications, where domain experts and stakeholders would really like more control and insight into how software works for them and others?\n\nThis approach implies a level of restraint, or a holding back of the generation of code that has not yet had this level of rigor applied to it. The discourse around vibecoding on the other hand seems to be the natural culmination of a “move fast and break things” philosophy that almost everyone outside of Silicon Valley has seen for what it is.",
  "title": "Proofs"
}