I'm doing several myself at an abstract level given lack of time or resources. I feed what I learn in them to pro's for potentially seeing it built. Here's a few:<p>1. Modula-2-style systems language with macros, better typing, and typed assembler to replace C with minimal hit on performance or ease of use.<p>2. Relatively-simple, imperative language plus translators to equivalent functionality in mainstream languages to leverage their static analysis or testing tools if possible.<p>3. Unified architecture to natively represent and integrate both imperative (C or Modula style) and functional (Ocaml or Haskell style) languages. Extensions for safety/security at hardware level for both.<p>4. Hardware/software development system using Scheme or abstract, state machines that can turn a high-level description into software, hardware, or integrated combo of both.<p>5. Defining TCB's for type systems, OS architectures, etc that minimize what must be trusted (mathematically verified) to ensure invariants apply while maximizing expressiveness. crash-safe.org and CertiKOS are more concrete, useful, and professional versions of what I'm getting at with 5.<p>6. Building on 5, a series of consistent ways of expressing one program that capture sequential, concurrent, failure, integration, and covert channel analysis in a clean way for formal analysis. As in, an all-in-one high assurance toolkit that automates the common stuff a la static analysis or reusable, composable proofs. And makes hard stuff easier for pro's.<p>7. Occasional thoughts on automatic programming via heuristics, patterns, rules, human-guided transforms, and so on. Got me started in advanced SW and my mind occasionally goes back to possibilities for achieving it.<p>8. A way to do any of that with the rapid iteration, safety, performance, live updating, and debugging properties of Genera LISP machine. I mean, we <i>still</i> don't have all that in mainstream tooling? ;)