TL;DR: Java’s multi-billion-dollar ecosystem is quietly dependent on a shrinking, fragile IDE infrastructure, and without deliberate investment beyond IntelliJ and Eclipse, its long-term developer productivity is at serious risk.
I think Library APIs are a good example. I've found myself in the situation where I do not care about the string representation (or can convert in a few places if necessary), but need to provide an interface for others that is as frictionless as possible. My instinct there was to be generic and use From/To traits, but it never felt quite right.
Reflections in Tree Calculus work differnt from lisp quote/unqote used here. It is a hunch, but I think Tree Calculus can implement this (if it is sound) (book pg 64 ff on quote), but not vice-versa.
As far as I know there is no Tree Calculus with (dependent) types, because types in Tree Calculus work different from main stream type theory (you internalize the type checker using reflection (see book pg 58), a bit like I did here with scheme: https://github.com/JanBessai/tcscheme).
One should mention the RustBelt project: https://plv.mpi-sws.org/rustbelt/ here. It was in place to develop a specification for Rust that is accessible for formal verification. I think that is the way to go, rather than semi-formal standadese language. I've some related background and would love to do it (given there was a good postion/pay).