4 ms·

The problem is that determining whether an ostensibly C (syntactically valid and typable) program is actually written “in C” is undecidable.

adrianN 10y ago
Almost any interesting property about programs is undecidable. Yet somehow programmers still write nontrivial programs. Undefined behavior in C sucks, but being its presence or absence being undecidable is not the main reason.
- catnaroek 10y ago
  > Almost any interesting property about programs is undecidable. It's only undecidable if the language makes it undecidable. For example, subject reduction is decidable in a type-safe language (EDIT: with decidable type checking, oops!), because the very definition of type safety means that typability implies subject reduction. Of course, not everything of interest can be made decidable in a general-purpose language, but the integrity of a language's basic abstractions should never be in question.
- haldean 10y ago
  The formalization of this idea is Rice's Theorem: https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem
  - catnaroek 10y ago
    Rice's theorem is a statement about partial functions, not programs. There exist decidable properties of programs: Is it of size less than N (for any suitable measure)? Does it finish in less than N steps (for a given fixed input)? Two syntactically distinct programs may compute the same partial function.
- dllthomas 10y ago
  Careful about what you're quantifying over. Any interesting property is undecidable in the sense that we will be unable to produce an answer for some programs. Nothing says that there can't exist plenty of nontrivial programs for which we can show the property holds.
  - taneq 10y ago
    Excellent point. This misconception is also the root of silly statements like "human intelligence is uncomputable because we can do things like tell whether a program will halt." No, we can solve specific cases of the halting problem, we can't solve the general case any more than a computer can.
    - dllthomas 10y ago
      > we can't solve the general case any more than a computer can While almost certainly the case, I'm not sure how we can demonstrate that this is true in principle without begging the question, if we're asking whether human intelligence is computable. I agree that all we have evidence of is that we can solve specific cases, and that this completely undermines the argument you're critiquing. This error also occurs more subtly. I had someone tell me that static type checking was basically useless because it couldn't even do something as simple as saying whether a program will halt. Nevermind, if we're demanding this of all programs, that neither can any other method of reasoning we're applying. (And also nevermind, if we're demanding this of an interesting subset of programs, that there are type systems that will tell us exactly that...).
  - adrianN 10y ago
    Just like there are plenty of nontrivial C programs where we can be sure that the behavior is defined. That's exactly my point.

adrianN 10y ago

Almost any interesting property about programs is undecidable. Yet somehow programmers still write nontrivial programs. Undefined behavior in C sucks, but being its presence or absence being undecidable is not the main reason.

catnaroek 10y ago
> Almost any interesting property about programs is undecidable. It's only undecidable if the language makes it undecidable. For example, subject reduction is decidable in a type-safe language (EDIT: with decidable type checking, oops!), because the very definition of type safety means that typability implies subject reduction. Of course, not everything of interest can be made decidable in a general-purpose language, but the integrity of a language's basic abstractions should never be in question.
haldean 10y ago
The formalization of this idea is Rice's Theorem: https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem
- catnaroek 10y ago
  Rice's theorem is a statement about partial functions, not programs. There exist decidable properties of programs: Is it of size less than N (for any suitable measure)? Does it finish in less than N steps (for a given fixed input)? Two syntactically distinct programs may compute the same partial function.
dllthomas 10y ago
Careful about what you're quantifying over. Any interesting property is undecidable in the sense that we will be unable to produce an answer for some programs. Nothing says that there can't exist plenty of nontrivial programs for which we can show the property holds.
- taneq 10y ago
  Excellent point. This misconception is also the root of silly statements like "human intelligence is uncomputable because we can do things like tell whether a program will halt." No, we can solve specific cases of the halting problem, we can't solve the general case any more than a computer can.
  - dllthomas 10y ago
    > we can't solve the general case any more than a computer can While almost certainly the case, I'm not sure how we can demonstrate that this is true in principle without begging the question, if we're asking whether human intelligence is computable. I agree that all we have evidence of is that we can solve specific cases, and that this completely undermines the argument you're critiquing. This error also occurs more subtly. I had someone tell me that static type checking was basically useless because it couldn't even do something as simple as saying whether a program will halt. Nevermind, if we're demanding this of all programs, that neither can any other method of reasoning we're applying. (And also nevermind, if we're demanding this of an interesting subset of programs, that there are type systems that will tell us exactly that...).
- adrianN 10y ago
  Just like there are plenty of nontrivial C programs where we can be sure that the behavior is defined. That's exactly my point.