alt Hacker Newsformal verification is great and all, but you can never make it as ergonomic as functional verification. this matters for agents and real people alike.
formal verification requires a deeper understanding of underlying mechanisms to write correctly. yet nothing prevents you or your agent from changing invariants to fit the algorithm and making it incorrect.
And neither can be made as ergonomic as no verification at all. It's all about how much you need. Functional verification isn't an appropriate tool where a single bug is catastrophic.
> yet nothing prevents you or your agent from changing invariants to fit the algorithm and making it incorrect.
If the thing we're trying to prove is ungrounded, it's trivially true that any verification method falls apart. You're still encoding priors in your testing methodology. No matter how robust you think your testing suite is, I can still trick it if given free reign over the codebase.