On 5 Feb 2025, at 19:03, Marc Nieper-Wißkirchen <xxxxxx@gmail.com> wrote:

>> I don’t see how this is the case. The implementation would somehow need to both inline the helper-proc (in order to do the re-ordering optimization you were worried about when you introduced the reference-barrier procedure) but also discard the reference-barriering nature of the mention of ‘key’. This seems very unlikely.
>
> It should be possible to prove the correctness of a program formally.
> For that, "very unlikely" is not enough.

It’s up to the compiler to do this correctly (or not), of course.

> That said, all semantics suggested so far have another problem, which
> I haven't mentioned yet: A reference barrier on the key in the
> unbroken case is useless. The GC can break an ephemeron if, under the
> assumption that it is broken, the key will not be kept alive.
>
> I am going to post a "real life" example soon (I am currently ill, and
> my brain is not fully working) so that we have some concrete code to
> test potential syntax against.

Okay, please do. I’m a bit confused by this. Get well soon!

Daphne