Ascent is lovely. The paper on it is really well written, too: https://s-arash.github.io/ascent/cc22main-p95-seamless-deduc...