Hacker News new | comments | show | ask | jobs | submit login

No, you're confusing "undefined" with "unprovable". There are several "safe" languages where every well-formed program has well-defined semantics (for example, most interpreted languages).

Undefined behavior means that there are some well-formed programs that have semantic holes: the specification says that is up to you to avoid that your program gets to some illegal state. If your program does, the language says "I told you not to get there. Now I can do whatever I want". The reason is that by assuming that the program cannot reach those states, better code can be generated (think bounds checking).

What Godel's theorem says (and the more CS-specific version of it is Rice's theorem [1]) is that you cannot have an algorithm that proves any given property about the semantics of a program. But if the language is safe, the property of being well-defined is trivial (all the programs have it), and trivial properties are the only exceptions to the theorem.

[1] https://en.wikipedia.org/wiki/Rice's_theorem




Correct. Rice's theorem limits the ability to check a program, e.g. with a compiler.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: