The GC algorithm that Nim originally implemented had a correctness proof and yet it was wrong... ;-)
And what's there to "prove" about the new runtime anyway? All the edge cases are found by implementing it. On paper the prove looks like: "Instead of use-after-free the RC mechanism counts all remaining unowned pointers to the object. These unowned pointers might or might not be used afterwards to trigger a use-after-free violation". That's all there is to it, the important questions are: * Is this annoying to use in practice? * Does it produce catastrophic crashes in practice long after the code has been tested extensively? > people will not invest in this language, since they know they are buying > something that is somehow on the verge of obsolescence. For how long will GC > be available when the new runtime is deemed to be stable? Yeah and before I started the --newruntime experiment people surely had no reason _not_ to invest in Nim. It's a terrible argument.
