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.
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
Putting limits on a scripting language should not be too hard (even without talking about any correctness proof). And I would bet that for a scripting language where the limits are in a way that "in a correct implementation, it should be highly likely that these limits are actually enforced" (i.e. the specification of the scripting language has no parts that makes you suspicious whether there exists some loophole that a malicious actor could use to overstep the limits), it should actually be possible to write a verified implementation with some effort.
But this is not what people want: for example, basically every evolution of the web standards since HTML5 by the WHATWG was about extending what is possible to do in the scripting language (JavaScript).
Management and marketing can only cope with a vague, third party description of the sheet.
A lot of modern programs never terminate and thus to me "halting" means no longer able to compute, i.e it's hung/deadlocked.
Computer Science historically being seen as a gateway to software development has done a large disservice to both fields.
And an astronomer should absolutely have understanding of those, their intricacies, the optical equations involved, and how to operate them (usually with automated software, but astronomers are the ones writing that software).
Now an astrophysicist has less to do with telescopes, especially if your field is theoretical cosmology, although they still require familiarity with telescopes, practicalities, how observations are made etc. because that is the basis of their theory. So, a cosmologist vs. an astronomer might be a better analog for a computer scientist vs. a software engineer.
And I know that despite doing my own thesis in cosmology, my studies involved a lot of knowledge and teaching about telescopes, including at least one night of observations (it's pretty boring, things are very automated).
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.
Roque de los Muchachos Observatory - https://en.wikipedia.org/wiki/Roque_de_los_Muchachos_Observa...
A heck of a lot. Your professor clearly does not know much about astronomy.
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.
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...
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.
I think those domains has more stringent requirement and a more focused usage, making the classes of inout narrower. A lot of software for B2B and B2C tries to be a kitchen sink and in the result get turned into a ball of mud. Some stuff should just be separate software.
This does not require proving systems complete correct, but it does involve proving many properties of these systems.
So I had to reconstruct a signal that fitted the data for the equations to work at all. But the reconstruction was no longer measured data. It was made up, and there was no single solution for fitting the data. That meant that, if I wanted, I could "respect the data" but output anything arbitrary.
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