Comment by devin
16 hours ago
Can you give me an example (real or imagined) where you're dipping into a bit of light formal verification?
I don't think the problems I work on require the weight of formal verification, but I'm open to being wrong.
16 hours ago
Can you give me an example (real or imagined) where you're dipping into a bit of light formal verification?
I don't think the problems I work on require the weight of formal verification, but I'm open to being wrong.
To be clear, almost (all?) of mine do not either and it's partially due to the fact I have been really interested in formal methods thanks to Hillel Wayne, but I don't seem to have the math background for them. To the man who has seen a fancy new hammer but cannot afford it, every problem looks like a nail.
The origin of it is a hypothesis I can get better quality code out of agents by making them do the things I don't (or don't always). So rather than quitting at ~80% code coverage, I am asking it to cover closer to 95%. There's a code complexity gate that I require better grades on than I would for myself because I didn't write this code, so I can't say "Eh, I know how it works inside and out". And I keep adding little bits like that.
I think the agents have only used it 2 or 3 times. The one that springs to mind is a site I am "working" on where you can only post once a day. In addition, there's an exponential backoff system for bans to fight griefers. If you look at them at the same time, they're the same idea for different reasons, "User X should not be able to post again until [timestamp]" and there's a set of a dozen or so formal method proofs done in z3 to check the work that can be referenced (I think? god this all feels dumb and sloppy typed out) at checkpoints to ensure things have not broken the promises.
I guess my feeling is that formal verification _even in the LLM era_ still feels heavy-handed/too expensive for too little value for a lot of the problems I'm working on.
I guess I am trying to think laterally right now. There’s a lot of attention given to crafting the right prompt to get what you need, but I am a belt and suspenders kinda guy and my concern is even if we get it right the first time, what guarantee do I have I don’t ask for a change a year from now without thinking through the implications and it subtly breaks stuff. There’s basically zero cost to me currently to require formal verification, as long as we don’t count the oceans I am helping to boil.