4 ms·

In a discussion I had recently we started talking about metaprogramming, which in practice is only the tiniest and most minimal execution of the implied idea: w

In a discussion I had recently we started talking about metaprogramming, which in practice is only the tiniest and most minimal execution of the implied idea: writing programs that operate on programs. Modern convention is to treat programs as black boxes that only the developers of that specific program can hope to reason about. And so metaprogramming is when a programmer writes or very carefully uses a component that operates on the program, but the result is just the program – you can't run the program without the applied metaprogramming nor can you apply metaprogramming to a program and expect it to work. Except debugging. Underneath the suggestion in the paper I see something similar. "Programming" might be an overly specific term. But a call to apply reasoning to systems and computation. Not applying reasoning to specific systems, as a programmer might analyze or test a specific program (what we're already doing), but to systems as a whole. I can see this in other computing developments. Operating systems are the result of reasoning about hardware. The result looks very different from coding directly to the hardware, especially in our mature state. But programs still are binaries with machine code. Before the OS of course was the program itself. And so what would it look like if we applied this kind of reasoning to programs? But oh, we already apply so much reasoning to programming! But in a certain way. We apply reasoning to compilers, which programmers use as they will. We build libraries and hope they are used well. And then we pull these together to some actual purpose in the program. And we assemble programs into systems. Each step empowers the next layer, but we don't apply (much) software to explore, verify, or extend these layers. Our tests are typically written as binary pass/fail systems, with no generalized attention to WHY something fails – and we can't apply generalized attention because the program is too opaque.

nickpsecurity 11y ago
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? ;)

nickpsecurity 11y ago

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? ;)