I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world. Any software that's processing inputs and provides complex workflows to humans has to necessarily deal with the endless vagaries of reality.

That's not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth...

I agree with you that for most software, verification was historically less of the requirement, however some software always needed to have abstract, mathematical correctness -- think military, medical, industrial automation.

While these areas were main premise of an article when it was written, I think the article really aged well into current time of mass AI/LLM deployment. It shows fundamental limitations of token based systems / symbolic reasoning that LLM espouses internally, while writing correct software. These limitations also apply to humans, however humans mental modelling, being not fully based on symbolic processing, have been historically shown capable of writing correct software systems, while AI/LLM systems have not been proven to be able to do that, and as article shows that with current token based technology it's unlikely they will ever be.

There is a wide range of software that exists in a "adversarial" environment, including anything facing a network or processing outside data. At a minimum, this software should should not allow an attacker to execute code of their choice on a system handling private data.

This does not require proving systems complete correct, but it does involve proving many properties of these systems.

Having been downvoted, I like to clarify that this comes from the experience working in finance with developers with a strong academic background that emphasized on the necessity of formal proof to a point where complexity made actual progress nearly impossible- while simultaneously basing the proof repeatedly on assumptions that did not uphold in practice.

Nah I don't disagree with you. Thing is even if you formally prove that for every input you produce a valid output. In safety certified software, there's the problem that if that input comes from a sensor, a sensor is an inherently probabilistic thing, and it may be that you will have false positives. The best you can do is build a safety case that even if you get false positives you end up in a safe state, but you can't guarantee that they won't ever increase operational costs.

what were some categories of such assumptions, can you name some examples?

a fun one that immediately comes to mind is asserting something holds for reals, but not evaluating whether it holds for IEEE floats, though maybe that's not really a thing in finance due to rounding related rules anyways

The real question is: for a typical program we prove it - even though we know there are programs we can't prove?

I don't care about the examples given, I care about my word processor, web browser and such. Can we prove them - putting limits on the scripting language

I was always interested in formal verification but have only written toy proofs and derived programs.

It's nice to see this older discussion of the topic outside of 'AI does lean' and the assumptions that formally verification is easy or will be easy for AI and you can just switch you brain off.

Build programs that can be verified in the first place is difficult design problem that requires real thought and deep insight of the problem.

Maybe it's just me but the terminology used in "halting problem" didn't age well.

A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.

A lot of the language of computer science doesn't translate well to software development.

Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.

I had a professor once say that a computer scientist has as much to do with computers as an astronomer has to do with telescopes.

Reminds me of the classic The Parable of the Toaster:

https://www.glaver.org/ftp/humor/toaster-fable.txt

I'm pretty sure its a quote from Dijkstra.

Tell him he knows little about astronomy and invite him to watch the latest episode of The Sky at Night - a bunch of astronomers gush over a diverse set of telescopes ...

La Palma - Gateway to the Universe (November 9, 2026)

  The team journey to La Palma, where giant new telescopes and cutting-edge science are opening extraordinary new windows on our universe.

~ https://thetvdb.com/series/the-sky-at-night/episodes/1205884...

Roque de los Muchachos Observatory - https://en.wikipedia.org/wiki/Roque_de_los_Muchachos_Observa...

> as an astronomer has to do with telescopes

A heck of a lot. Your professor clearly does not know much about astronomy.

I think the point is that yes, of course telescopes are important to astronomers, but they're not the essence, they're not what the study is about. They are the tools of the study, not the object of the study.

The same can be said about computers and computer science. I don't think I fully agree with that, but it's interesting to think about.

Don't astronomers use telescopes?

And yet, the amount of slop I've seen produced to solve a problem that is trivially reduced to e.g. graph traversal on more than one occasion is astounding. I tend to think it's got more advantages than disadvantages and we should be gatekeeping harder.