edsl VS parsejevko.py

I'm taking a brief detour from working on my actual language to work on some underlying theory. My language (Sligh) is based on informal certifying compilation, i.e. the compiler generates a test checking for correctness of the compiled program instead of a proof. Because I'm mostly interested in generating code for full-stack web applications, I think optimization is actually essential for the practicality of this approach, otherwise the certificate test will be much less effective.

So, full compilation of the implementation is out in my mind, and the next best thing is at least deriving the implementation from the model so you can leverage the logic you've already defined. That's where metaprogramming comes in, and that's what I'm playing around with here.

I tried sketching one out in Python: https://github.com/jevko/parsejevko.py ; one in C: https://github.com/jevko/parsejevko.c ; one in Java: https://github.com/jevko/parsejevko.java ; one in Scheme: https://github.com/jevko/jevkostream.scm (that's a streaming parser stub, more fleshed out one in JS is here: https://github.com/jevko/jevkostream.js ); and there are some implementations of Jevko formats and other related things in the GitHub organization: https://github.com/jevko