Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Any algorithm can be made to create "yes", "no", and "I don't know" buckets, and all undecidability means is that "I don't know" cannot be empty. I don't really know of any case where undecidability truly caused people to shy away from attempting to solve problems: static analysis is frequently undecidable and yet it's a fairly thriving field.


As a hard result, undecidability may be unimportant. Someone rarely wants to know whether a Gödel sentence is "true" or determine whether a program that references itself halts.

But such theorems, by placing a theoretical, if contrived, limit, often seem to have a qualitative implication as well: namely that solving the problem in the general case, even if we manage to exclude pathological cases, is hard or even unfeasible.

It seems consistent with the fact that there is no known algorithm for deciding whether a theorem is true, or for accurately and fully predicting the behaviour of arbitrary programs. As you said, that doesn't make formal methods useless. But it reframes the discussion away from trying to find a universal problem solver towards discussing tradeoffs (e.g. pushing the proof burden to the programmer, rejecting valid programs, or using imperfect heuristics).




Consider applying for YC's Winter 2027 batch! Applications are open till November 2.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: