Skip to content

Comment on C*: Unifying Programming and Verification in C (2025)parent

Comments

The problem I've been having is the LLM's are super dodgy, not even ten minutes ago the 'solution' to a proof failing was to disable that check in the static analysis harness so the tests pass since their first try (with a counter example and lemma from the literature in hand) didn't fix the issue.

Maybe it's an issue because it controls both sides of the fence and can change things willy-nilly when it thinks I'm just watching the youtubes but I haven't been able to find a another way to do this so, here we are...

You might find Round-Trip Correctness: A New Metric for Generative AI-Based Process Modeling useful - https://news.ycombinator.com/item?id=49033317

Also see resources at https://news.ycombinator.com/item?id=49269323

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.