On Tuesday, 17 June 2014 at 22:44:00 UTC, Timon Gehr wrote:
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,
It will single out exactly the programs that are most certainly memory safe, and also single out those programs that have generated unsafe features (instructions). Whether those unsafe features sit in a basic block that will never called is a different matter since @safe does not address that.
So yes, @safe is not equivalent to memory safety, it is equivalent to the absence of FEATURES that can lead to situations that aren't memory safe. But that is splitting hairs.
Absence of features such as unsafe instructions is a trivial property of the compiled program. A non trivial property is whether the program terminates, returns 0, rejects the input "hello", etc.
and invoking Rice's theorem to this end is perfectly fine and does not suffer from any 'issues'.
Not really, you can prove termination for all programs with 3 instructions and 3 bytes of RAM. You can do it for all programs with 4 instructions and 4 bytes of RAM. You can do it for all programs with N instructions and N bytes of RAM. You cannot do it for all TMs since they have unbounded storage.
Thus you can prove non-trivial properties such as whether a functions returns with 1, whether it accepts or rejects the input '0', etc. It might take a lot of time, but you can do it in a fixed amount of time. You cannot do it for TMs.
But this issue is simpler than that. Think about it this way: There are problems that have a solution, but it is provable impossible to solve analytically. You still can solve them numerically down to a specified precision.
I posit you can do the same with memory safety, as in: you can reject all unsafe programs and reduce the set of false positives to a marginal set of typical programs (which are written with memory safety in mind).
