Two things: first, it's very impressive that you're doing the hard work to integrate this with IDEs and such. To me that shows that you're really serious about getting real-world uptake. There are a few tools and systems that do what you're doing but most of them never seem to make it out of some tiny niche and remain academic.

Second, your Marvin sub-project, if I understand it correctly, is just awesome. Congratulations.

In re: Truffle, and lang-to-AST conversion in general, I've taken a winding path over the better part of the last twenty-odd years. The closest thing to a serious idea I have to offer is this: Use Lisp as your inter-language AST.

I'm grinning but I'm not quite joking. ;-)

Think it through. What are the pros and cons?

(I can't help but mention, I'm working on a system that may one day "eat" other software and translate it into essentially an AST. The AST is actually just code in a language called Joy that resembles Forth+Lisp. The language is very simple and can be implemented on top of other languages in a few days. So I can (eventually) read in other code to this Joy/AST, clean it up, then run it on whatever substratum makes sense for a given use-case. Joy code is easily refactored, and can be fairly easily converted to logical relations and then you can use e.g. Prolog or miniKanren to search for optimizations. This is sort of "one step beyond" type inference, moving into the more esoteric but useful things where you can do partial evaluation and "super-compilation" (chase down alternate control-flow paths) to improve the abstract code and emit specialized e.g. assembly or LLVM IR or JVM bytecode or whatever.

My motivations are two: I want to teach normal people to program, and I want to contract the total amount of [distinct] software in the world, eliminating incorrect code and collecting, refining, and curating all correct code into a single unified codebase.

The Joy notation is easy enough to teach to normal people. I've created a simple GUI that presents a Joy environment where users can build new commands (Joy code). The system uses type inference to prevent the user from executing commands that won't work with the current system state, and to prevent the construction of new commands that won't work at all. It's impossible to make incorrect code in this (virtual) world.

The Joy language is highly-factorable, enabling a kind of "semantic compression". It's also Categorical (in the sense of Category Theory), meaning that programs in Joy represent abstract computations over categories and can deliver multiple correct programs for the same Joy expression. For example, the type inferencer works by evaluating Joy expressions over a category of stack effects and type variables to generate the stack effects of the expressions. Conal Elliot has a paper "Compiling to Categories" where he's exploring this sort of thing using Haskell, converting it to a "point-free" Joy-like notation and then implementing categories for dataflow diagrams and circuit descriptions and other cool things, to produce those all from the same original Haskell code.

I'm hopeful that I've got something here. :-) I've been sitting in a room in front of a computer for about a year and I'm just at the point where I have to go out and talk to people about it. Egad.

Anyhow, that's part of why I'm so impressed with what you've accomplished (and are no doubt going to accomplish!) I look at what you've done already and I think, "Daaaamn, this dude is running circles around me." Makes me feel sheepish, but I'm stoked for you! You're bringing the fire down from Olympus my Promethean friend, don't doubt it.