On Thursday, 19 June 2014 at 20:47:16 UTC, H. S. Teoh via
Digitalmars-d wrote:
programs!). So the only remaining approach is to consider all
possible
programs. Which means you have to implement exhaustive state
space
search. Which is impractical for the reasons I stated.
No. Is a program compiled to asm.js memory safe? It has to be,
because Javascript is a memory safe environment. You might still
mess up badly, but you can obviously transform just about any
program that is presumed to be memory unsafe into one that is
memory safe (if you consider a function to be a mapping of input
to output).
Are you telling me that you cannot write an equivalent mapping
from input to output using memory safe primitives while staying
within P? You can safely insist on only having access to valid
memory safe primitives within @safe and still be able to solve
the exact same problems, in pretty much the same way (on an
abstract algorithmic level).
It's not like @safe guards against exceptions IIRC. You can
inject bound checks everywhere and it is provable memory safe.
@safe should guarantee that your program terminates in an orderly
fashion without corrupting memory. @safe does not guarantee
correctness. That would be a folly.
A hypothetical and pointless "not @safe" does not guarantee
memory corruption either. If you compile to asm.js you obviously
always stay memory safe.
Or do you define "out of array bounds" exceptions as memory
corruption?
Now, if we were talking untransformable machine language, you
might have a point, not sure. But we aren't talking machine
language, we are talking D.
