Tail pad optimization, cache friendlyness and C++ interrop

[via Digitalmars-d]

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).