4:23:36beachnyef: What are you working on these days?
4:24:49nyefNo current major projects, though I'm still thinking about compiler verification, bootstrapping environments, and the like.
4:25:16nyefJust started thinking about "concatenative languages" and possible verification for them.
4:25:29beachI see. What is the direction of thinking with respect to bootstrapping environments?
4:27:38nyefHand-verifying that a Forth environment conforms to specification is a straightforward task. Given a proof logic that runs in such an environment, even if it's "just" a spoon-fed verifier, then that gives the first couple of links of a chain of trust.
4:28:26nyefSo, treat a "Forth-like" system with a real typing regime as a "kernel" language, and implement a more-normal environment on top of that.