@rocky from our Slack channel shared this a few days back. I felt it was worth sharing here
Writing Reverse Polish scripts sort of sucks, but to start off with it's what Bitcoin script does, so it isn't that intolerable by folks who do Bitcoin scripting. The Etherium scripting language, Solidity, is much nicer and it would not be too hard to do something like that which compiles to the Bitcoin script VM. But this is separable. Coq is cool, and seems like a good thing to prove an implementation has desirable characteristics, but that too is separable. And incremental. There is no prototyping benefit for proving the implementation correct and it bogs things down especially when there isn't a clear spec for either the VM or the language for that. I think if that by verifying that the each VM opcode is safe, and that the interpreter loop safe and bounded. Then that shows that any sequence of valid VM opcodes is safe. We might also have to prove some characteristics for parsing to VM, e.g. that parsing doesn't create an infinite loop. But would be part of a phase only after the VM works (minimally), and after the parser works(minimally) which is even after that. And again this is separable from everything else. Computing max time and max memory limits fis pretty easy, after each opcode has time amd memory requirements associated with it. The AST for the program is a tree, and one can compute requirements with a simple traversal of the tree. This too is separable and can be done later. Ok so now down to the meat of what needs to be done first. First step that would be useful is nailing down additional VM instructions. It looks like there is free opcode space in the bitcoin VM spec. Generally I prefer to build on existing work rather than reinventing from scratch, except when there is good reason to redo. If I have it correct, additional opcodes to Bitcoin script would be: opcode inputs output stacked ---------------- ----------------------------------------------- --------------- OP_NAME_REGISTER: <name> <value> <pay_account_id> <zonefile_hash> ? boolean OP_NAME_UPDATE: <name> <zonefile hash> ? boolean OP_NAME_TRANSFER: <name> <account_id> ? boolean OP_ACCT_SEND: <value> <account_id> ? boolean OP_NAME_METADATA: <name> <metadata> ? OP_STORE_DATA: <data> ? OP_MINE_BLOCK: <hash> <account_id> <coinbase value> <scratch area> ? OP_FIELD_ZONEFILE_HASH: <id> hash OP_LOADNAME <hashed id> ?? OP_FIELD_METADATA: <data> field metadata OP_HASH_LSTACK ? ? For those above that are correct, it would be great to describe the inputs, outputs and what each opcode does with (when possible) links to other blockstack documentation. Something akin to https://en.bitcoin.it/wiki/Script#Crypto Keep in mind that the behaviour might include an immediate failure with no stack output instead of a boolean unconditionally. How does one capture time and resources for something like OP_MINE_BLOCK? Is the data in OP_STORE_DATA unlimited? If so one will have an unbounded limit for that. So a rough (with emphasis on "rough") idea of the time and memory resources for these operations would be nice. For the various hashing code, we'll also have to fill something like that in. Eventually. Also, it would be good to prioritize opcodes in those that would have the most benefit for a prototype. If there are just one or two opcodes that will show a lot off that'd be great. I started modifying The Bitcoin IDE to add an opcode. (I added OP_HASH0 which the identity hash and is useful in testing scripts) As an IDE for testing scripts it is fine, but one needs to consult the Bitcoin Script reference implementation as well, since I found the semantics can differ. OP_EQUALVERIFY in the IDE is identical to OP_EQUAL which is incorrect as per the reference implementation since the former should raise an invalid transaction and terminate while the latter doesn't'. But for the real thing, one wouldn't use this. Personally, initially I'd probably prototype in Python as that has to interface easily in a number of ways with blockstack which is also in Python. But at some point I'd switch to a compiled language (Rust and Go are the obvious choices), not just for speed and low runtime overhead and to allow execution in limited environments.