3 ms·

Asking as someone who's never spent significant time/effort working with Gtk/GObject in C (only a bit in Python). Isn't it still generally desirable to have the

Asking as someone who's never spent significant time/effort working with Gtk/GObject in C (only a bit in Python). Isn't it still generally desirable to have the compiler yell at you, if you can't convince it you know what you're doing? Rather than allowing the possibility of memory corruption. I do agree that the code in the example is far from beautiful. I wonder if we were to redesign GObject from scratch, if we could make interfacing with Python, Rust, JS, etc a bit less hairy.

Someone 5y ago
The work you have to do to show your compiler that certain constraints hold (say that i and j point inside the same array and that i < j can be extremely cumbersome, even in cases where it’s obvious that they do hold. That makes it not seem worth the trouble. Of course, that obvious may turn out to be incorrect for some edge condition. Basically, that’s the same reason why mathematicians don’t put all proofs through a proof assistant.
- tialaramex 5y ago
  Of course, to the extent you assumed things the machine didn't test that. The core of TLS 1.3 was proved before it shipped. But, the proof makes an assumption which has consequences. It assumes when communicating using an agreed shared secret† you have a separate shared secret for every such pairing. So Alice and Bob need a shared secret but (and this is where humans trip up compared to what was actually proved) the proof says Bob and Alice also need a shared secret different from the one for Alice and Bob. The consequence of this accidentally missed assumption is the Selfie attack. Alice and Bob share a secret S and communicate over the Network using TLS 1.3. Bob fed the cat half an hour ago. The cat has employed Mallory to trick Alice into feeding it even though Bob already did. Alice sends a message on the Network. It is encrypted with S and it says "Did you feed the cat?". Mallory doesn't know S and can't read this message or tamper with it. But Mallory simply redirects the message back to Alice. Alice receives a message, properly encrypted using S, which says "Did you feed the cat?". She presumes this message is from Bob, so she answers "No, go ahead and feed the cat". Mallory redirects this response back to Alice too. Alice receives "No, go ahead and feed the cat" and she concludes Bob hasn't fed the cat so she feeds it again. Oops. The proof was fine, but we brought an assumption along that we did not clearly articulate. † You never use this mode in your web browser, but IoT things might do this because it's easier than all that stuff with certificates.
- southerntofu 5y ago
  > The work you have to do to show your compiler that certain constraints hold In rust, that's what the unsafe keyword is allowed. It doesn't mean that the code is actually unsafe, but rather that the compiler should trust you on this one.

Someone 5y ago

The work you have to do to show your compiler that certain constraints hold (say that i and j point inside the same array and that i < j can be extremely cumbersome, even in cases where it’s obvious that they do hold. That makes it not seem worth the trouble. Of course, that obvious may turn out to be incorrect for some edge condition. Basically, that’s the same reason why mathematicians don’t put all proofs through a proof assistant.

tialaramex 5y ago
Of course, to the extent you assumed things the machine didn't test that. The core of TLS 1.3 was proved before it shipped. But, the proof makes an assumption which has consequences. It assumes when communicating using an agreed shared secret† you have a separate shared secret for every such pairing. So Alice and Bob need a shared secret but (and this is where humans trip up compared to what was actually proved) the proof says Bob and Alice also need a shared secret different from the one for Alice and Bob. The consequence of this accidentally missed assumption is the Selfie attack. Alice and Bob share a secret S and communicate over the Network using TLS 1.3. Bob fed the cat half an hour ago. The cat has employed Mallory to trick Alice into feeding it even though Bob already did. Alice sends a message on the Network. It is encrypted with S and it says "Did you feed the cat?". Mallory doesn't know S and can't read this message or tamper with it. But Mallory simply redirects the message back to Alice. Alice receives a message, properly encrypted using S, which says "Did you feed the cat?". She presumes this message is from Bob, so she answers "No, go ahead and feed the cat". Mallory redirects this response back to Alice too. Alice receives "No, go ahead and feed the cat" and she concludes Bob hasn't fed the cat so she feeds it again. Oops. The proof was fine, but we brought an assumption along that we did not clearly articulate. † You never use this mode in your web browser, but IoT things might do this because it's easier than all that stuff with certificates.
southerntofu 5y ago
> The work you have to do to show your compiler that certain constraints hold In rust, that's what the unsafe keyword is allowed. It doesn't mean that the code is actually unsafe, but rather that the compiler should trust you on this one.