One of the real eye openers for me along that journey was realizing that Eclipse refactors were (mostly, except for some rough edges) automated semantic invaria

One of the real eye openers for me along that journey was realizing that Eclipse refactors were (mostly, except for some rough edges) automated semantic invariant preserving code transformations, which is to say a kind of simplified equational reasoning resting solely on the equivalence. Equational reasoning is borderline magical, and I look forward to the day when it's as pervasively taught as basic logic. I have this fantasy in my mind of a language/editor combination that begins with the empty program and only allows legal equational development. Without explicit predication that would just maintain the invariants of the language itself, so no undefined behaviors, but with user supplied predicates would allow a kind of exploratory programming with safety nets. One way to look at it would be explicit symmetry breaking, although I'm not sure that's a good way to describe it to typical working programmers. The idea though is that for a program with the empty specification all code transformations are symmetrical with respect to the spec. And then as the specification is added to certain transformations become symmetry breaking and thus illegal, with said illegality being statically checked. Clearly I'm waving my hands quite a lot here, and I have no clue if it's actually practicable.