Called this a little bit: https://fly.io/blog/semgrep-but-for-real-now/

Semgrep isn't a formal methods tool, but it's in the same space of rigor-improving tooling that sound great but in practice are painful to consistently use.

anyone interested in this i suggest reading this

https://github.com/jegly/self-supporting-code

Unlikely. It's more work than necessary and systemic/cultural change follows the path of least resistance. Formal verification is a new thing a programmer would have to learn, so nobody will want to do it. They'll just accept the resulting problems as "the cost of AI".

Or the alternative will happen: people will stop using AI for programming. It's not actually better than hiring a person, it's just supposedly cheaper (in that you can reduce staff). That's the theory anyway. Yes there will be anecdotes from a few people about how they saved a million dollars in 2 days or something like that, the usual HN clickbait. But an actual study of the impact of using AI for programming will probably find it's only a marginal cost savings and isn't significantly faster.

And this is assuming the gravy train that programmers are using (unsustainable spending/building in unreasonable timeframes for uncertain profits) keeps going indefinitely. Best case, when it all falls apart the govt bails them out. Worst case, you won't have to worry about programming because we'll all be out of work from the AI bust recession.

There's really no such thing as complete verification.

The quest for purity is some fountain of youth nonsense that distracts a lot of otherwise brilliant engineers.

Ask the AI to make a program that consumes a program and determine if it halts.

You can’t even compile regular code with satisfying speed

AI is great; it makes my job easier by removing repetitive processes, freeing me up to tackle other "stuff". I like that I can have it form up json/xml scaffolding, etc. All the insanely boring stuff that can often get corrupted by human error.

AI isn't the solution to move humanity forward in any meaningful way. It is just another aspect of our ability to offload labor. Which in and of itself is fine. Until of course it gets weaponized and is used to remove the human aspect from more and more everyday things we take for granted.

It is being used to accelerate the divisions among people. Further separating the human from humanness. I love 'AI' tools, they make my life easier, work-wise. But would I miss it if it wasn't there? No. I did just fine before and would do so after it's flame and innovation slowly peters out.

Will formal verification be a viable and profitable avenue for the middle man to exploit and fuck everybody else? Then yes, it absolutely will become mainstream. If not, them no, thanks. Everything that becomes mainstream for SURE will empower the middleman and cuck the developer, nothing else really matters. This is literally the only important factor.

No - I don't want AI to be "mainstream".

that just testing code noo ???

what makes it different other than called it "verification" ???

i agree, i wrote a z3 skills for claude and generate a proof before writing code