> 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.

> 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.