| 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: 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. 2. Relatively-simple, imperative language plus translators to equivalent functionality in mainstream languages to leverage their static analysis or testing tools if possible. 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. 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. 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. 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. 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. 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 still don't have all that in mainstream tooling? ;) |