Thank you so much for taling the time to write this thoughtful and valuable reply! It helps me see what I think I’m seeing, or rather to define it. It also has

Thank you so much for taling the time to write this thoughtful and valuable reply! It helps me see what I think I’m seeing, or rather to define it. It also has helped me to perspectives I hadn’t seen. I’m coming to dependent types from here: “simple, clear code good yes program program argh I can’t express a very distinct thought without escaping to another language layer or generating code using string concatenation”, and from here: “my data structure is simple and clear but argh it needs a handwritten parser and serializer and it needs to be maintained and argh why am I writing a parser AND a serializer it should be just one bidirectional definition? and argh why do I need to write it for each output/input format?”, and from here: “my code is simple and clean and my variables are well named and my tests are well defined and my documentation is well written but argh why can’t I just fold the mechanics that the tests define into the code? as proofs? (and… argh? why can’t my variables and documentation and method names be checked against the code?)”. It’s metaprogramming that I’m thinking about. And most programming ought to be programming. But we definitely need metaprogramming, and it needs to be understandable and composable and simple and clear. And I don’t know if dependent types are a complete solution to that, but I do think that they are necessary for it. That-which-is dependent types, which by definition is a computation of what it is and is a proof of what it is. Those philosophical terms finally become practically grounded and practical help in a lot of the work I find myself doing. I’ll certainly look for the false idol too! My sincere thanks.