After 7 Months, Glasswing Overwelms Maintainers with Underwhelming Findings

Re:After 7 Months, Glasswing Overwelms Maintainers with Unde... by Paracompact on Tuesday November 10, 2026 @09:07PM (#50448996)

The bar for Turing-complete is very low. The halting problem is to programming as Godel's incompleteness theorem is to metamathematics. Yet no one is seriously suggesting that we downgrade to axiomatic systems incapable of expressing Peano arithmetic, nor that our current axiomatic systems are impractical for proving theorems.

We cannot automatically and completely verify nontrivial semantic properties of arbitrary programs written in a Turing-complete language (Rice's theorem), but as long as we as humans can intuit correctness arguments for our programs, then formal methods will apply to it. Of course, declarative rather than imperative programming semantics tend to result in simpler correctness arguments, sidestepping reliance on global state and convoluted loop invariants.

[ Parent | on HN ]

Re:After 7 Months, Glasswing Overwelms Maintainers with Unde... by Ohentis on Wednesday November 11, 2026 @10:03AM (#50454294)

I just don't think we need turing completeness to solve the problems we try to solve with software. You bring up how humans can reason and prove correctness for our programs, but I say we just force them to do that (making our programs no longer turing complete). I don't think I've ever encountered a problem that required steps that I didn't think I would be able to prove halted.

[ Parent | on HN ]