I think I'm still failing to adequately explain what I mean. Let me try being absurdly explicit. The following is ordinary Rust code, and the reader is supposed to pretend that the two functions prefixed with valen_ are in Valen instead.

    #[derive(Default)]
    struct Receiver<'a> {
        ref_and_val: Option<(&'a u32, u32)>
    }
    
    impl<'a> Receiver<'a> {
        fn set(&mut self, reference: &'a u32) -> ()
        {
            self.ref_and_val = Some((reference, *reference))
        }
        
        fn check(&self) -> ()
        {
            if let Some((reference, val)) = self.ref_and_val {
                if *reference != val {
                    panic!("The impossible happened!")
                }
            }
        }
    }
    
    fn valen_inner_fun<'a>(r: &mut Receiver<'a>, val: &'a u32)
    {
        r.set(val)
    }
    
    fn valen_intermediate_fun<'a>(r: &mut Receiver<'a>, val: &'a mut u32)
    {
        // In a real mixed-language example, this would be in Valen, not Rust,
        // and it would declare a mutable effect on val.
        valen_inner_fun(r, val);
    
        // And it would do this, which Rust disallows.
        *val = 17
    }
    
    fn main() {
        let mut r: Receiver = Receiver::default();

        let mut fortytwo = 42;
        valen_intermediate_fun(&mut r, &mut fortytwo);
        r.check()
    }

This compiles except for the *val = 17 line. (rustc's error message is a bit confused, and maybe I'll file a bug about that. If one follow's rustc's advice, the weird error turns into a less weird error.)

My point is that Receiver::set() requires a promise that its parameter's referent is immutable for the entire lifetime 'a, which exceeds the lexical duration of set() itself. And valen_outer_fun in Rust knows this to be true as a result of Rust's shared-xor-mutable system, and Rust's borrow checker verifies this:

a) the code would compile if I removed the offending *val = 17

b) the code, correctly, does not compile as written

c) If I force the issue by replacing *val = 17 with:

    unsafe { *(val as *const u32 as *mut u32) = 17 }

then it panics and we can all imagine we're using C++ instead of Rust :)

But valen_inner_fun does not mutate val, and if I understand right then this means that Valen would accept its Valen equivalent without mut(val), and this seems unsound to me.

When I first thought of this, I imagined set() instead being a work-dispatching function that would run its passed-in closure and hit UB due to a data race with the *val = 17 line, and my edit was my realizing that there's a simpler non-concurrent example.