I feel like we will continue to run into these kinds of issues to the end of time unless can figure out: 1. How to precisely describe the properties we want the

I feel like we will continue to run into these kinds of issues to the end of time unless can figure out: 1. How to precisely describe the properties we want the final system to have, 2. How to 'compile' from a higher-level language/layer into a lower-level language while maintaining all those properties. At the least this will require us to: 3. Define the precise semantics of each layer and enforce that every construction in and implementation of that layer adheres to it strictly. Properties like "no private data is accessible until the user consents", "the final result of the algorithm is independent of the order that messages are received", "decryption must be constant-time and the program must not have any observable effect until the message is known to be verified", etc. Obviously these properties as stated are incomplete and imprecise, but that's my point: we have to figure out how to make these kinds of statements precise enough. Layers/languages should verifiably maintain these properties through every translation via paths like: eula/privacy policy, requirements, UX, UI, state machine, source code, AST, IR, ASM, machine code. Every one of these layers should have a well-defined execution model that is isomorphic with other layers, modulo metadata. For example: source code === AST [+ comment/whitespace/filesystem metadata], AST === IR [+ name/desugaring/applied-optimizations metadata]. All undefined behavior at every layer must be exterminated by definition or avoided by construction. One problem is that we throw away too much metadata when moving between layers which makes the task of maintaining these properties through many layers extremely difficult. For example, trying to implement constant time algorithms in a high-level language is nearly impossible to hold over time (robust to changes in source and compiler) because the compiler/optimizer has forgotten (or was never told) what parts must be done in constant time and to not use the partial results of the algorithm until it has completely finished. To implement this, all candidate implementation strategies and optimizations in the lower layer must be identified by whether they preserve constant time execution or not, and optimizer/compilation unit (CU) boundaries inserted to prevent an over-eager optimizer for a non-constant-time CU to observe partial results. Etcetera for every other desirable property and every layer.