Could open source activity transition towards provably correct software, with far more modest feature sets?

I don't have experience with proof based tools, so I'm not sure what's feasible.

A lot of people in the open source world actually enjoy the act of programming. Not all of them will enjoy prompting to the same degree, but to keep pace with the bad guys you will have to either join or find something else to do. That's going to be a big loss.

▲

rectang 28 minutes ago | parent [-]

It's funny, that's true although I personally can't relate — I enjoy having built something robust, but the act of building isn't something I love.

I can imagine prompting an LLM to build provably correct software. Aren't we already doing something similar already when we remind it to write unit tests and account for all edge cases?

Actually writing provably correct software from scratch sounds terribly tedious, which is why I've never explored it. But maybe an LLM could make that task more approachable.

	▲	jacquesm 24 minutes ago \| parent [-]
		I switch between the two modes. I love algorithmic stuff and I really don't like working on boilerplate and plumbing. So I use AI for the second and read every line and all the other stuff I roll by hand. The speedup isn't super like that but the amount of control is pretty good.