Why should it need one?
back
1 comments
To support freeing heap allocations in a memory-safe way without relying on a GC.
Here another one: https://news.ycombinator.com/item?id=17601789
Looks like that is effectively a borrow checker. So, the reason to need one still seems valid.
You asked for a BC in Ada, but this is SPARK, which we use for formal verification of Ada code, so there is no need to also have it in Ada; besides that you can do much more in SPARK than just BC and even Ada has much more powerful type features than any other language which in very many cases makes memory management or pointer handling unnecessary (e.g. you can declare much more things by value on the stack, even with variable lenght data structures).
> You asked for a BC in Ada, but this is SPARK, which we use for formal verification of Ada code, so there is no need to also have it in Ada;
Sorry, I didn't. I was just pointing out why you'd want a borrow checker. I think you might be referring to another poster.
Oops, my bad.