I agree and have proposed the same thing. I was trying to build on my old toolkit which aimed at RAD w/ C/C++ compatibility, BASIC safety, and LISP flexibility. I essentially implemented a basic-like language that was compatible with C/C++ functions in LISP. Let me have LISP macros and interactive development with result auto-generating C/C++ code that reused their compilers. Worked great while I had it. I know the BASIC angle is funny to many. However, it's how I started & iterated fast with readable, no blue-screen code. I'd have used a Wirth language if I knew of them then.
So, next question was "How to make an environment to allow easier development of high assurance, portable systems?" My platform was a 4GL w/out 4GL's problems. I want a 4GL for highly-secure or reliable software. Noticed portable by itself usually requires a bunch of variations on same basic thing. LISP macro's handled that for me prior. So, my concept was to use something like Racket Scheme for meta while building a mockup of constructs of imperative language (Wirth's, Go, or C). Transformations for specific systems are encoded as meta transforms that operate on base program.
Initially, the thing just generates code it feeds through existing compilers. From there, you model the basic constructs (eg control flow, stacks) in both a generic form and one optimized for certain situations (or ISA's). Language abstractions are modeled as compile-time transforms on these. Constraints, pre/post conditions, invariants, and so on are added as needed for next phase: type/interface checking + automatic production of verification conditions, tests, static/dynamic checks, covert channel analysis, and so on based on annotated code. Each refinement uses data in step before it for correspondence check (eg trace-based). Ends at typed assembly (or LLVM maybe) modeled in same system subject to same correspondence checks and extra analysis at that level. Any run reuses what's already done and not changed while supporting multicore to reduce run time. Critical checks run in background as developer modifies the software.
Written and specified to high level with metaprogramming transforming, analyzing, and optimizing it to lowest levels. Highest, assurance levels using tools such as Coq or HOL would be able to leverage HLL code for easier, spec-to-module/code mapping while trusting certified transforms to do the rest. Your thoughts aside from how much work this might be? ;)
So, next question was "How to make an environment to allow easier development of high assurance, portable systems?" My platform was a 4GL w/out 4GL's problems. I want a 4GL for highly-secure or reliable software. Noticed portable by itself usually requires a bunch of variations on same basic thing. LISP macro's handled that for me prior. So, my concept was to use something like Racket Scheme for meta while building a mockup of constructs of imperative language (Wirth's, Go, or C). Transformations for specific systems are encoded as meta transforms that operate on base program.
Initially, the thing just generates code it feeds through existing compilers. From there, you model the basic constructs (eg control flow, stacks) in both a generic form and one optimized for certain situations (or ISA's). Language abstractions are modeled as compile-time transforms on these. Constraints, pre/post conditions, invariants, and so on are added as needed for next phase: type/interface checking + automatic production of verification conditions, tests, static/dynamic checks, covert channel analysis, and so on based on annotated code. Each refinement uses data in step before it for correspondence check (eg trace-based). Ends at typed assembly (or LLVM maybe) modeled in same system subject to same correspondence checks and extra analysis at that level. Any run reuses what's already done and not changed while supporting multicore to reduce run time. Critical checks run in background as developer modifies the software.
Written and specified to high level with metaprogramming transforming, analyzing, and optimizing it to lowest levels. Highest, assurance levels using tools such as Coq or HOL would be able to leverage HLL code for easier, spec-to-module/code mapping while trusting certified transforms to do the rest. Your thoughts aside from how much work this might be? ;)