Compiling
Interpreting Runway models in JavaScript is slow, and that harms the simulator and model checker. We should be able to do better by compiling down to JavaScript/asm.js/WebASM. Eventually, especially for model checking, we'll want to compile down to a specialized model checker and/or C/Rust/Go.
For a simulation target, using a language with a garbage collector will make things easier than trying to worry about generating code with the appropriate malloc/free pairs. It's also not clear in what cases it will be possible to produce code to execute the simulation directly, or if the end result will be the same simulator but written in a faster language. A hand-written example of what this might look like using Go as the backend: https://github.com/dgryski/modelchecking/tree/master/go
For a model checker target, using a language that support the constructs in runway is probably easier than having to simulate them. For instance, the collections API would need to be implemented in Promela (spin) as it does not natively have those types. This could be done via embedded C code: http://spinroot.com/spin/Man/c_code.html
