> Concurrency is impossible to prove sound without language-level guarantees.

Not sure I understand that. The proposal is not to simply get rid of the GIL, but to have a two-tier mechanism that ensures correctness with all the C source that uses the macros it should use and doesn’t mess with refcounts behind Python’s back (doing sketchy stuff usually ends up in pain)