3 ms·
But that doesn't directly relate to the verifiability of milliForth itself. An extremely shortened code can be harder to verify, for example it may work as inte
by lifthrasiir 3y ago
But that doesn't directly relate to the verifiability of milliForth itself. An extremely shortened code can be harder to verify, for example it may work as intended unless a very specific input is used to break out of its sandbox (so to say). Bootstrapping needs a short and readable enough seed for that reason, and I can't be entirely sure that it is indeed the case for milliForth.
- taneq 3y agoThe sneakiest possible program representable in n bytes is never less sneaky than the sneakiest possible program representable in n-1 bytes, assuming you can pad a program out with nops.
- lifthrasiir 3y agoYou don't need a sneaky program, you only need a program that misbehaves on sneaky inputs.
- taneq 3y agoThose are the sneakiest programs.
- alexisread 3y agoTechnically I guess what you'd do is hand type in binary code to create a hex editor, then bootstrap this forth off that, by hand-typing it in. If you include formal verification tools as part of the stack then you can verify the tools by eye, type them in, and use them to verify the function of the stack. Admittedly Forth is tricky to do here, but something like lisp/scheme/wat can actually be proven out with say microkanren. From there we can trust the software stack.