On 06/17/2014 11:50 PM, "Ola Fosheim Grøstad"
<ola.fosheim.grostad+dl...@gmail.com>" wrote:
...
Btw, Rice's theorem is based on the halting problem for TMs… so it
suffers from the same issues as everything else in theoretical CS when
it comes to practical situations.
There is no such 'issue', or any meaningful way to define a 'practical'
situation, especially such that the definition would apply to the
current context. Theoretical computer scientists are saying what they
are saying and they know what they are saying.
Whether generated IR contains unsafe
instructions is trivially decidable. Since you can define an IR in a way
that discriminate between unsafe/safe instructions you can also decide
that the safe subset is verifiable memory safe.
As you know this will not single out _exactly_ the subset of programs
which is memory safe which is the claim I was arguing against, and
invoking Rice's theorem to this end is perfectly fine and does not
suffer from any 'issues'. The kind of thing you discuss in this
paragraph, which you appear to consider 'practical' is also studied in
theoretical CS, so what's your point?
