News for hackers. Stuff that matters.

A comment on Prediction: AI will make formal verification go mainstream. Parent comment

Re:Prediction: AI will make formal verification go mainstream by est on Wednesday December 17, 2025 @02:42AM (#46299258)
> It cannot tell you if the spec if good

I beg to differ, if a spec is hard to verify, then it's a bad sign.

[ Parent | on HN ]
Re:Prediction: AI will make formal verification go mainstream by MattHeard on Wednesday December 17, 2025 @03:29AM (#46299528)
it can tell you if your spec is bad, but it can't tell you if your spec is good
[ Parent | on HN ]
Re:Prediction: AI will make formal verification go mainstream by Joker_vD on Wednesday December 17, 2025 @03:38AM (#46299585)
All non-trivial specs, like the one for seL4, are hard to verify. Lots of that complexity comes from interacting with the rest of the world which is a huge shared mutable global state you can't afford to ignore.

Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories but seriously.

[ Parent | on HN ]
Re:Prediction: AI will make formal verification go mainstream by jessoteric on Wednesday December 17, 2025 @04:06AM (#46299749)
> Of course, you can declare that the world itself is inherently sinful and imperfect, and is not ready for your beautiful theories

i see we are both familiar with haskellers (friendly joke!)

[ Parent | on HN ]