Yet another leak in the sinking ship of @safe

[Timon Gehr via Digitalmars-d]

On 18.02.2016 19:41, H. S. Teoh via Digitalmars-d wrote:
> On Thu, Feb 18, 2016 at 07:30:34PM +0100, Timon Gehr via Digitalmars-d wrote:
>> On 18.02.2016 17:37, H. S. Teoh via Digitalmars-d wrote:
> [...]
>>> 1) Casting an array of elements with indirections (in this case
>>> Object[]) to void[] is questionable at best, outright unsafe at
>>> worst, as shown here. Even if we were to rewrite readData() and mark
>>> it @trusted, it still raises the question of what a @trusted function
>>> can legally do with void[], which is essentially a type-erased array,
>>> that justifies being tagged as @trusted.  How can a function do
>>> anything that doesn't break @safety if all type information about the
>>> array has been erased, and it essentially sees it only as a ubyte[]?
>>> I'm inclined to say that @trusted functions should only be allowed to
>>> receive const(void)[] as parameter, not void[].
>>>
>>> 	https://issues.dlang.org/show_bug.cgi?id=15702
>>>
>>
>> No problem here. There is no way to assign to a void[] without doing 2.
>
> Sure there is:
>
> 	void breakSafety(void[] data) @safe
> 	{
> 		union U {
> 			void[] d;
> 			int[] arr;
> 		}
> 		U u;
> 		u.d = data;
> 		u.arr[0] = 0xFF; // kaboom
> 	}
> ...

That's in essence just a different way to cast void[] to int[]. Steven's 
example disproves my previous claim though. Still, I don't think the 
conversion is the problem. It's the mutation of memory without type 
information.


>
>>> 2) To add salt to the wound, though, blatantly casting void[] to T[]
>>> is allowed in @safe code, thus, readData() can even get away with
>>> claiming to be @safe, when in fact it is anything but.
>>>
>>> 	https://issues.dlang.org/show_bug.cgi?id=15672
>>
>> This is the culprit.
>
> It's only one of many culprits. As long as there is any way around
> @safe, the entire system of guarantees breaks down.
>
>

If you want to verify guarantees, @safe should be specified by inclusion 
and ideally, type safety should be proved formally (after applying a few 
fixes). This first requires a formal language semantics.
That's already a lot of effort, and after that you still don't have a 
verified implementation.