@gassahara@mstdn.io Compiler writers are also human! Intention of not only the standard but of programming languages (and mathematics) is primarily human to human communication. You need to be able to read what I wrote, otherwise it's useless. Yes It's not a teaching material, it's a reference, but the agreement on it is where the portability comes from fundamentally. It doesn't seem human only because it's a very big relationship.

Stroustrup's friend Stepanov also convinced me that C++ style generics is the way to go with programming in general (hehe, "general").

@amiloradovsky@functional.cafe Yes reailty is imperfect, and we must yell at it, so that others hear us and be convinced. That is all that matters.

Coq still seems way beyond my comprehension, too many steps the purpose of which is unclear to me. When it comes to formal systems I think mathematicians have a lot more work to do there first, maybe using Coq.