On Wednesday, 9 December 2020 at 13:25:49 UTC, Timon Gehr wrote:
> On 09.12.20 12:46, Dukc wrote:
>> 
>> It might have some benefit: If non-annotated C libraries are considered `@safe`, it'll mean that not-so-quality code is using compromised `@safe`. Bad. But if they are considered `@system`, not-so-quality code will not be using `@safe` AT ALL. Even worse.
>
> That's a bit like saying it's bad if products produced using slave labour don't get a fair trade label.

You're thinking `@safe` as a certificate. It can definitely help in doing certifying reviews, but it's also supposed to be a tool to catch mistakes - for all code, not just for code that wants to certify. That it won't catch mistakes from using the C code does not prevent it from catching other unrelated mistakes. That's still better than nothing if we don't pretend that the C headers are certified.

One can still add a comment to describe why the code is annotated `@safe` or `@trusted`.

On Wednesday, 9 December 2020 at 14:05:44 UTC, Paul Backus wrote:
> Using compromised @safe is much, much worse than not using @safe at all. Not using @safe at all means you still have the option of migrating to @safe in the future. If you're using compromised @safe, you have no migration path.

Yes you have, assuming you have documented appropriately. Look for comments saying "greenwashed as @trusted" or whatever, and recheck the annotations of those places.

Note that I meant internal usage. With library APIs you're right. Yeah, I quess that's another problem with Walter's DIP. but personally I think that if the APIs would have been annotated within 6-12 months of the DIP acceptance, the blame of the breakage would be on the library user. And if it took longer, the library was probably abandoned anyway.

On Wednesday, 9 December 2020 at 13:28:14 UTC, Timon Gehr wrote:
> On 09.12.20 14:06, Paul Backus wrote:
>> On Wednesday, 9 December 2020 at 08:29:58 UTC, Bruce Carneal wrote:
>>> [...]
>> 
>> This does not work for extern(C) functions because their names are not mangled.
>
> It does not even work for extern(D) functions because their return types are not mangled.

I did not know this.

If we lose information when we compile separately it's over.  If you can't close the proof you've got no proof.

On Wednesday, 9 December 2020 at 15:56:18 UTC, Dukc wrote:
> Note that I meant internal usage. With library APIs you're right. Yeah, I quess that's another problem with Walter's DIP. but personally I think that if the APIs would have been annotated within 6-12 months of the DIP acceptance, the blame of the breakage would be on the library user. And if it took longer, the library was probably abandoned anyway.

Ultimately, breakage is breakage. It doesn't really matter who the blame falls on; it's still a problem.

On Wed, Dec 09, 2020 at 04:02:46PM +0000, Bruce Carneal via Digitalmars-d wrote:
> On Wednesday, 9 December 2020 at 13:28:14 UTC, Timon Gehr wrote:
> > On 09.12.20 14:06, Paul Backus wrote:
> > > On Wednesday, 9 December 2020 at 08:29:58 UTC, Bruce Carneal wrote:
> > > > [...]
> > > 
> > > This does not work for extern(C) functions because their names are
> > > not mangled.
> > 
> > It does not even work for extern(D) functions because their return
> > types are not mangled.
> 
> I did not know this.
> 
> If we lose information when we compile separately it's over.  If you can't close the proof you've got no proof.

This has nothing to do with separate compilation.  The C ABI simply does not encode parameter or return types, needless to say function attributes.  The D ABI does not encode return type information, because doing so would imply overloading by return type, which is not possible in D.

You cannot "prove" anything in the way of proving it down to the raw machine level.  At some point, you have to depend on the consistency of the layer below you.  Just because you mangle return types, does not prevent lower-level breakage of your proof.  For example, you can declare a @safe function at the D language level, but link it to a C function that just happens to have the same name as the mangled D name, and you're free to make this C function do whatever you want, and there's nothing the compiler can do to enforce anything.  Just because the mangled name says it's safe, does not guarantee it's safe.

Even if you somehow require the D compiler to take over the entire process down to the executable, bypassing the system linker, that still guarantees nothing.  I can use a hex editor to modify the executable after-the-fact to break the @safe-ty proof, and there's nothing the compiler or the language can do about it.  Even if you somehow "protect" your executable, I can run it on a modified OS that edits the program in-memory while it's executing, and there's nothing the language can do about it either.

Basically, the automatic verification of @safe, etc., relies on the consistency of the lower-level layers. It does not "prove" anything in the absolute sense.  You might be able to do that if you invent your own hardware from ground up, starting from the transistor level.  But you can't do that with a programming language that's intended to run on a large variety of preexisting systems.  Just like in mathematical proofs, you can only prove down to the axioms, you cannot prove the axioms themselves.  If the axioms are violated, your proof collapses.  The guarantees of @safe only hold if certain assumptions about the lower-level layers hold; however, there is nothing you can do to guarantee that.  You cannot prove your axioms, you can only assume them.


T

-- 
I see that you JS got Bach.

On Wednesday, 9 December 2020 at 16:34:28 UTC, H. S. Teoh wrote:
> On Wed, Dec 09, 2020 at 04:02:46PM +0000, Bruce Carneal via Digitalmars-d wrote:
>> On Wednesday, 9 December 2020 at 13:28:14 UTC, Timon Gehr wrote:
>> > On 09.12.20 14:06, Paul Backus wrote:
>> > > On Wednesday, 9 December 2020 at 08:29:58 UTC, Bruce Carneal wrote:
>> > > > [...]
>> > > 
>> > > This does not work for extern(C) functions because their names are
>> > > not mangled.
>> > 
>> > It does not even work for extern(D) functions because their return
>> > types are not mangled.
>> 
>> I did not know this.
>> 
>> If we lose information when we compile separately it's over.  If you can't close the proof you've got no proof.
>
> This has nothing to do with separate compilation.  The C ABI simply does not encode parameter or return types, needless to say function attributes.  The D ABI does not encode return type information, because doing so would imply overloading by return type, which is not possible in D.

If you compile from source @safe can be enforced because the compiler has all the information it needs.  However things are represented in .o files and libs, if that representation does not give you the necessary information then you can't enforce @safe mechanically.

>
> You cannot "prove" anything in the way of proving it down to the raw machine level.  At some point, you have to depend on the consistency of the layer below you.  Just because you mangle return types, does not prevent lower-level breakage of your proof.  For example, you can declare a @safe function at the D language level, but link it to a C function that just happens to have the same name as the mangled D name, and you're free to make this C function do whatever you want, and there's nothing the compiler can do to enforce anything.  Just because the mangled name says it's safe, does not guarantee it's safe.

I agree. If your information is probabilistic then you do not have a hard proof.

>
> Even if you somehow require the D compiler to take over the entire process down to the executable, bypassing the system linker, that still guarantees nothing.  I can use a hex editor to modify the executable after-the-fact to break the @safe-ty proof, and there's nothing the compiler or the language can do about it.  Even if you somehow "protect" your executable, I can run it on a modified OS that edits the program in-memory while it's executing, and there's nothing the language can do about it either.

No one can prove anything about a system that is modified after it leaves the proof domain.  Does anyone believe otherwise?

>
> Basically, the automatic verification of @safe, etc., relies on the consistency of the lower-level layers. It does not "prove" anything in the absolute sense.  You might be able to do that if you invent your own hardware from ground up, starting from the transistor level.  But you can't do that with a programming language that's intended to run on a large variety of preexisting systems.  Just like in mathematical proofs, you can only prove down to the axioms, you cannot prove the axioms themselves.  If the axioms are violated, your proof collapses.

Does anyone think otherwise?

> The guarantees of @safe only hold if certain assumptions about the lower-level layers hold; however, there is nothing you can do to guarantee that.  You cannot prove your axioms, you can only assume them.

Again, I don't see this as an issue.  As you note, there is nothing any proof system can do when the "axioms" are violated. We're not trying to prove that all HW is correctly implemented, for example, or that it can withstand cosmic rays, or a power spike or, for that matter, that an arbitrarily patched binary has any properties at all.

I agree that, even within the compiled language domain, "proof" is probably better thought of as aspirational rather than literal.  There may be errors in the "proof": compiler implementation errors, language definition ambiguities/errors that were "correctly" implemented, and probably other modes of failure that I've not thought of.

However, I do not agree that because we can not prove everything we should stop trying to prove anything.

Finally, thanks for bringing up some of the hazards of using the word "proof" wrt computer systems.

>
>
> T

On 09.12.20 16:42, Dukc wrote:
> On Wednesday, 9 December 2020 at 13:25:49 UTC, Timon Gehr wrote:
>> On 09.12.20 12:46, Dukc wrote:
>>>
>>> It might have some benefit: If non-annotated C libraries are considered `@safe`, it'll mean that not-so-quality code is using compromised `@safe`. Bad. But if they are considered `@system`, not-so-quality code will not be using `@safe` AT ALL. Even worse.
>>
>> That's a bit like saying it's bad if products produced using slave labour don't get a fair trade label.
> 
> You're thinking `@safe` as a certificate.

It is, that's why it's on the function signature and causes function type incompatibility. `@safe` has an actual modular meaning that is communicated to the caller; it's not supposed to be just a collection of lint heuristics. It's supposed to contain all memory-safety errors within `@trusted` functions.

> It can definitely help in doing certifying reviews, but it's also supposed to be a tool to catch mistakes - for all code,

No, this feature does not exist currently, it is not the way @safe has been advertised, and separating code into @system/@trusted/@safe would make no sense if it was. You'd just want different strictness levels with no modular guarantees at all for most of them.

If that's useful to you, feel free to advocate for it, but this is not what `@safe` is.

> not just for code that wants to certify. That it won't catch mistakes from using the C code does not prevent it from catching other unrelated mistakes. That's still better than nothing if we don't pretend that the C headers are certified.
> 
> One can still add a comment to describe why the code is annotated `@safe` or `@trusted`.
> 

You can't have the documentation state one thing and silently start practicing the opposite. It's a plain, corrupt lie. Why is this not obvious? You'll be right back in fairy-tale wonderland where good programmers don't make mistakes and everyone else does not matter.

On Wednesday, 9 December 2020 at 18:20:48 UTC, Timon Gehr wrote:
[...]

Not to reply your post in particular but a general reply. I couldn't care less about this @safe lobbyism, it really doesn't do anything for me. @safe is just a limitation of the features in D so it isn't really safe or maybe it will be somewhere in the distant future. Rust started this safe nonsense but in reality your program is as safe you make it, it's just a word that is being used for marketing. Java and C# are just as safe but didn't use that kind of marketing because programmers understood what they are about anyway.

Programming languages today seem to be victims of "Objects in mirror are closer than they appear" jargon. In reality you will not be safer because of that stupid sentence, which the rest of world don't seem to need.

I don't really care what happens to the @safe DIP as long as I have an easy escape from it. If you want to be safe, don't do what I do like changing the stack pointer in the middle of the execution. Which would be perfectly ok in @safe code with DIP 1028 as changing the stack pointer is done via a assembler function. I don't really mind because if I mess up, it's my fault.

On Wednesday, 9 December 2020 at 18:20:48 UTC, Timon Gehr wrote:
> On 09.12.20 16:42, Dukc wrote:
>> You're thinking `@safe` as a certificate.
>
> It is, that's why it's on the function signature and causes function type incompatibility. `@safe` has an actual modular meaning that is communicated to the caller; it's not supposed to be just a collection of lint heuristics. It's supposed to contain all memory-safety errors within `@trusted` functions.
>

I quess the stance on this is where the fundamental disagreement about C code default `@safe`ty lies. If one considers, even in internal code, that `@safe` and `@trusted` are always declarations that calling it can never corrupt memory unless there's a honest mistake in the implementation, your stance on this is perfectly sound.

But as it can also work as a limited down-and-dirty bug-finder, I really think we should consider it as a valid use case. While continuing to consider use as a certifying aid valid alike.

On Wednesday, 9 December 2020 at 20:30:57 UTC, Dukc wrote:
>
> I quess the stance on this is where the fundamental disagreement about C code default `@safe`ty lies. If one considers, even in internal code, that `@safe` and `@trusted` are always declarations that calling it can never corrupt memory unless there's a honest mistake in the implementation, your stance on this is perfectly sound.

The meanings of @safe and @trusted are spelled out in the language spec. [1] They are not a matter of opinion.

[1] https://dlang.org/spec/function.html#function-safety

> But as it can also work as a limited down-and-dirty bug-finder,

@safe does not find bugs; it prevents them.