I think it will kill open source to some degree. I found it already very hard to imagine how the endless queues of issues were being dealt with so diligently, but at least there was a human on the other side. The torrent that is unleashed now is not manageable on a human scale. It's a highly automated arms race with a bunch of good-willing humans caught in the crossfire between large companies and criminals duking it out.

▲

rectang 2 hours ago | parent [-]

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.

▲

jacquesm an hour ago | parent [-]

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 an hour 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 an hour 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.

▲

rectang 16 minutes ago | parent [-]

I just gave this prompt to duck.ai (5.6 Terra under the hood): "How would one go about writing a provably correct algorithm to count UTF-8 code points?"

It gave me something which looked pretty legit. Of course, the generated output very likely to be subtly wrong, but as starting input to a formal checked specification/proof process it seemed like a good start.

I wrote some UTF-8 based string handling software back in the day. It doesn't seem unreasonable to write up a set of requirements and edge cases and then have a formal mechanism prove correctness for common UTF-8 string manipulation operations.

[PEAK HN ON] Now if we could just write provably correct exception handling, we could solve one of the two PHP vulns from today. [PEAK HN OFF]

	▲	jacquesm 10 minutes ago \| parent [-]
		UTF8 is one nasty little standard. So many edge cases. I should check it against my email address validator that would be a nice benchmark. It's interesting that there are people that are using email addresses that are not actually valid according to the standard.