On Friday, 27 February 2015 at 09:33:43 UTC, Kagamin wrote:
If you can't give an example of unsafety easily, that's already quite important. Compare to C, where one can provide such an example easily.
Yes, that is true. Also, if you are conservative in C++ you also get pretty good safety with unique_ptr etc. So weak memory safety is ok, but then I also think it is ok to provide @trusted convenience since you are already saying that the programmer is competent:
unsafe_malloc!T() unsafe_free!T() unsafe_memmove!T() unsafe_mmap…
If you want to write a mathematical prover, that won't hurt, though such tools don't need language support, lints and provers were written even for C.
Yep. But what I meant is that a type system (including memory safety) ought to be proven sound. I.e:
1. You construct a simple language/type-system P and prove that P is sound and safe. 2. You construct a transform T(x) that can transform language D into x.
=> D is proven safe.
