[flagged]
Formal methods and the future of programming
71–80 of 129 posts
Re: Formal methods and the future of programming
#72I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-…
> how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer. ... How do y…
With the proof checker.
Re: Formal methods and the future of programming
#73I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which…
Have you looked at ADA Spark?
If you have does it match your intuition of how things should be done?
I am slowly working on something where I hope to integrate such a capability for the things that type systems can't handle quickly.
So I would be interested in perspectives of people who have been down this route before.
Re: Formal methods and the future of programming
#74I was playing around with stuff trying to get Claude produce a JavaCard VM with the idea that the VM was hand written from the spec with a separate, independently produced, spec file used to generate tests for ESBMC to verify so an identical bug would have to exist in both to make it through. Worked out pretty well, found a few bugs in both projects, but my poor laptop can't handle the full 32-bit space so that part never got the full verification -- 16-bit, rock solid though.
Then I really got serious about the yak shaving and, well, am probably in need of an intervention as I don't get Claude to write a VM but to make the tools to generate a VM from an assortment of DSL and that has snowballed a bit as I really liked shaving yaks before the daffy robot revolution.
--edit--
Almost forgot, I tried that with the little less dodgy banned Claude and the wasm standard it wrote a python script to parse the spec pdf, the official bytecode implementation in OCaml (or whatever) and generate a TOML file (Claude loves the TOML) to generate the type headers and for cross-referencing in the other tools. Was so impressed I just let it go on its merry way and it did the deed.
Re: Formal methods and the future of programming
#75In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Now, since it's impo…
You have to see it from janestreet's perspective. They're an HFT and trading high volume (millions if not 10's of millions) of stock & instruments. There is no "fix". By the time you understand what's wrong you've lost billions.
So yeah - offensive may work in non-critical areas.
Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.
I was wondering when we would start seeing formal verification. It makes sense that we would go from worrying about implementation details to a scientific/mathematical description of the problems.
Re: Formal methods and the future of programming
#76I think it's a good time to learn Lean. It positions itself as a proof assistant that's also good at practical programming. I'm not sure how mature the ecosystem is for the latter.
Re: Formal methods and the future of programming
#77Earlier quoted context omitted.
> I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Nice, I like the term too. But the paradigm is absolutely status quo in the industry. The thing is: with Gen AI the cost of "defensive programming" has gone way down, while the cost of (human) verification has gone way up. On the other hand, formal methods make verification cheap but come with massive imple…
You're right. I think the point we need to discuss here is, to be clear, dividing the contexts in which defensive programming is strong and where it should be aggressive. I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe. In that…
> I think the overhead of implementation is enormous, but I believe AI can write it. However, before even reaching the 'implementation' stage, that is, at the planning stage, sufficient data must be collected for the implementation to be safe.
I don't really follow here, I think once you know what you want the system to do, you could start to model it formally. What data do you think needs collection for planning here? Is it just for performance profiling of whatever algorithms are decided on? But that seems equally as relevant as if you do your initial implementation straight-up in code w/o any formal approach.
Re: Formal methods and the future of programming
#78In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Now, since it's impo…
You have to see it from janestreet's perspective. They're an HFT and trading high volume (millions if not 10's of millions) of stock & instruments. There is no "fix". By the time you understand what's wrong you've lost billions. So yeah - offensive may work in non-critical areas. Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your…
>Fwiw - you already use defensive everywhere. Python, Java, etc. come with garbage collectors. It's verified that the code is executing your intent.
Sort of. Garbage collectors can be fallible too, especially where release optimization is used.
Re: Formal methods and the future of programming
#79Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. I guess doing things twice can help catch errors, but I fail to see what’s so special about formal specs if they can suffer from the exact same bugs as the tests/implementation. I guess the root of the problem is if you want to formally prove t…
The powerful difference is between specific testing and exhaustive proving. If you fail to think of a test for an edge case, whoops. If you have a good model, you can know that it exists—and fix it—before you ship.
This is particularly valuable IMO in concurrent/distributed/multi-threaded situations where race-conditions and deadlocks are extremely hard to test and reason about. "Can A, B, C happen in the order 'A, C, B'" types of things.
I have a rough hypothesis that maturity in this space looks something like:
1) LLMs will allow much faster learning and usage of formal methods, even if initially just for "do it a second time" post-hoc verification
2) From there you move towards automation of LLM-checking "hey, the implementation code changed, does it look like it broke the model" - though this is still not deterministic, but it's likely a lot better than a human review requirement of something that only changed infrequently would've been
3) And then the real jump will be taking tooling for "write just the formal spec, let the implementation get generated" to the next level. There's various mostly-not-fully-baked-for-what-most-companies-would-want projects already out there for codegen like this, what if the LLM tools can accelerate the year-or-two of manual work it would take to make one of them fit your needs?
Re: Formal methods and the future of programming
#80Earlier quoted context omitted.
>Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?
Non trailing whitespace means the string doesn't end with a space. But foo is a function that converts an AST to a string, that's totally different. Or it's a function that loops until \0 and changes all spaces to + The spec should be a summary of what the impl is supposed to do. You'd want more than just doesn't end with whitespace of course.
> Non trailing whitespace means the string doesn't end with a space
No. And this is a great example of the problems with specifications. You still have to write a spec. And this, too, is subject to bugs.
What's wrong with the statement above is there are 17 space characters in Unicode and another eight whitespace characters, like newline.
If you try to verify that something ends in whitespace, you have to make sure you have the right definition.
Not picking on parent poster! It's just a great example of the fact that you can verify, but if what you are verifying is wrong, it doesn't help.