Hacker News Reader

Comment by ChrisGreenHeur | Hacker News Reader

Yay let’s lock ourselves into the formal verification toolsets, so that we can never use new language features again.

When you board a plane, don't you love thinking about how the controllers can make use of the hottest new language features? Perhaps JSON in the stdlib?

Would you board a plane designed by AI that no engineer had ever looked at?

Or some engineer did give a cursory glance at and stamped it with LGTM?

Yes. Correct software is more important than developer convenience.

Business value is more important than correctness

OR new languages and frameworks ever again, since they'll slow down code generation due to lack of training, and from LLM generation standpoint this is a terrible thing to trade off.

Both this and the parent takes are exceedingly odd - don’t you think that it’d lead to the language features also just getting the same proofs, as well as better libraries and frameworks? And do you not think that this would also lead to the LLMs both outputting better code since they’d be trained on the verified stuff and also because we’d have tooling to let agent loops autonomously resolve most of the issues with what they output?

I’d rather wait 5-10 years for a stdlib way of handling JSON, XML, YAML, TOML and other formats than using unproven libraries made with unserious practices that have edge cases. The same applies for processing requests, doing any sort of multiprocessing, DB interaction, validations, hell even any and all front end work all they way down to CSS. Don’t even get me started on desktop and server software and OS stuff.

Maybe then software engineering can be treated like real engineering.

Reply on news.ycombinator.com