> abstract, human-evaluatable, programming language? yes, it's happening: https://ncatlab.org/nlab/show/Globular https://ncatlab.org/nlab/show/Globular > Use

> abstract, human-evaluatable, programming language? yes, it's happening: https://ncatlab.org/nlab/show/Globular https://ncatlab.org/nlab/show/Globular > Use logically derived variable names I agree. It just becomes a pain in the ass to write this stuff. The greek is math-asm for the hand. > completely standard way as to how to define all of your algorithms and logical assertions? people are working on it, for example: https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath "This coq library aims to formalize a substantial body of mathematics using the univalent point of view." One thing to note however is that the mathematics in the OP is inherently two (and higher) dimensional, and so it makes much more sense to adopt a language that is two (or higher) dimensional. Squashing it down into one dimensions (like with a usual language) creates a big mess.