Comment by gavinray

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 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.

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...