Test, don't just verify
alperenkeles.com
Test, don't just verify
1–10 of 146 posts
Re: Test, don't just verify
#2Alperen,
Thanks for the article. Perhaps you could write a follow-up article or tutorial on your favored approach, Verification-Guided Development? This is new to most people, including myself, and you only briefly touch on it after spending most of the article on what you don't like.
Good luck with your degree!
P.S. Some links in your Research page are placeholders or broken.
Re: Test, don't just verify
#3> AI-assisted programming pushes the limits of programming from what you can implement to what you can specify and what you can verify.
This really resonates. We can write code a lot faster than we can safely deploy it at the moment.
Re: Test, don't just verify
#4> AI is making formal verification go mainstream.
This nonsense again. No. No it isn’t.
I’m sure the people selling it wish it was, but that doesn’t make it true.
Re: Test, don't just verify
#5Alperen, Thanks for the article. Perhaps you could write a follow-up article or tutorial on your favored approach, Verification-Guided Development? This is new to most people, including myself, and you only briefly touch on it after spending most of the article on what you don't like. Good luck with your degree! P.S. Some links in your Research page are placeholders or broken.
I'll add some links for the original VGD paper and related articles, that should help in short term. Thank you! I'll look into writing something on VGD itself in the next few weeks.
Re: Test, don't just verify
#6> AI is making formal verification go mainstream. This nonsense again. No. No it isn’t. I’m sure the people selling it wish it was, but that doesn’t make it true.
LLM-style AI isn't great for formal verification, not so far as I understand. And the recent advances in AI didn't do much for the kind of AI that is useful for formal verification.
Re: Test, don't just verify
#7Related discussion from last week:
AI will make formal verification go mainstream
Re: Test, don't just verify
#8[dead]
Re: Test, don't just verify
#9I think this misses a lot of reasons why learning verification is important. For instance learning the concept of invariants and their types such as loop invariants. They make reasoning about code in general easier, even if you never formally do any verification, it makes it easier to write tests or asserts(). A substantial amount of bugs are due to the program having a different state to that assumed by the programmer, and there are other tools that help with this. For example a statically typed language is a type of verification since it verifies a variable has a specific type and thus operations that can be performed on it, and limits the valid input and output range of any function. Languages like Rust are also verification in terms of memory correctness, and are also extremely useful tools.
Re: Test, don't just verify
#10Formal verification is a nice idea but it's a big hill to climb from where we're at. Most people can't even get agents to robustly E2E QA code, which is a much smaller hill to climb for (probably) larger benefits. I'm sure this area will improve over time though, since it is an eventual unlock for fully autonomous engineering.