@amiloradovsky@functional.cafe @gassahara
"The mpn functions are designed to be as fast as possible not to provide a coherent calling interface", Doesn't sound very promising, though I wouldn't be surprised if GMP has very similar abstractions to what I'm talking about here. I'm saying a better version of those lowest level abstractions should be standard. I would even strive to make the operators work with that.

Coq I'm not familiar with, but It didn't seem very generic to me from your posts, sounded like a very specialized environment, where you can allow yourself to (or even have to) ignore a whole lot of reality. I don't want to make my own perfect world, I want to code to a standard. Rather than reinventing all the wheels, my time would be better spend writing one of those completely ignored proposals for the c++ standard, if I ever get around to it.