Hacker News Reader

Comment by gavinray | Hacker News Reader

I really think that verification aware languages are going to become a necessity

Wrote a bit about this recently

https://gavinray97.github.io/blog/design-by-contract-and-eff...

The first thing people need to study is the "Correct by Construction" approach to programming as espoused by Edsger Dijkstra. Only then will the mathematical concepts used in verification aware languages start making sense and one can better understand what and how to use it.

One of the best books to learn this from is The Correctness-by-Construction Approach to Programming by Derrick Kourie and Bruce Watson - https://link.springer.com/book/10.1007/978-3-642-27919-5

The book actually uses Dijkstra's GCL language and wp-calculus along with Carroll Morgan's Refinement Calculus to demonstrate step-wise derivation of programs from specifications using a lot of examples.

I totally agree. I have this nagging feeling that LLMs push things like this past the breaking point. Effects and contracts are _obviously_ useful to humans as well, we've just gotten by without them for a long time. But when you have intelligence on demand, context building is a huge bottleneck, and local reasoning becomes way more useful from an efficiency perspective.

I'd love to see some actual experiments with LLMs in this area. There are a fair number of languages with effect implementations at this point.

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

I've been looking at model checkers and program proof assistants on and off since FDR and Isabelle/HOL and the like, and there were similar tools going back another decade before that. If you're verifying part of an ASIC or a crypto protocol or something similar they're fine (if extraordinarily painful to use), but for anything else they've been bypassed by AI. I'm not saying that as an AI fan but because by the time you get your PhD and then spend another five years learning how to use the tool and mark up the code and hope you got the markup right and after another six months of what feels like trying to make a string go in a certain direction by pushing it and the tool finally finds a nonexploitable buffer overflow in a function that's never called you realise you could have done the same thing with $2 in AI tokens. It's the program verification technology of the future, and always will be, while "claude, find places where this code does things it shouldn't" is right now and doesn't require a PhD to use.

Reply on news.ycombinator.com