Stumbled on this when trying a hypothetical compiler for bootstrapping that would be “obviously correct” without heavy formal methods. Inspired by Prolog and K Framework, I wanted to just do something that matched on patterns and substituted. Term rewriting and some metaprogramming do this. The best route on correctness seemed to be breaking everything down into simplest steps possible running sequentially as usual. Each has guard conditions. Each operates on AST. Pull the text into the interpreter, run through the rules one at a time, you’re done when none does anything, and dump the result back out. Looking up obscure models of computation, I stumbled on one, the Markov algorithm, that does the same thing. Also stumbled across this IDE in the process.
Well, I guess I’ll look into those a bit since people beat me to the idea. I’ll be surprised if they’ve maxed out its utility given how long it took for someone to do KCC compiler. The one problem my design had was that the compiler analyses needed before best applying certain rules don’t really fit the model. I’m not sure if there will be a clean way to integrate them. Worst case, I’ll make them built-in functions that rules can activate which, upon running, add either specific rules to execute or extra information in the program tree for rules to act on. I think I might also see ways to fit them in the model when I get around to actually learning metaprogramming, logic programming, etc where I’d be forced to try. It is fun seeing what I can do from imperative and ASM models, though. :)
EDIT: Turns out Mr. Turchin already built something similar in the 1960’s. It uses pattern matching and substitution to operate on trees just like mine. Submitted it separately. Brilliant given he didn’t have much prior work to go on. Now I remember his name from someone talking about supercompilation and cybernetics. I find Refal much more understandable. :)