"It is actually a fairly amazing tool" Since I watch formal methods from a distance, I can't really tell how good their approach is versus Microsoft's VCC w/ s

"It is actually a fairly amazing tool" Since I watch formal methods from a distance, I can't really tell how good their approach is versus Microsoft's VCC w/ separation logic, Coq specifications, and so on. I just note they seem to have it easier than most like Coq with their method more flexible than separation logic. How hard do you think it would be for a non-formalist programmer to learn K and start modeling interpreters or compilers in it? Anything you'd recommend to a person trying to learn it in terms of background material? "One problem with building semantics for Rust is that the language doesn't have a sufficiently formal specification yet." My solution there was to make the semantics represent the current state of Rust and/or LLVM at any moment. They got the advantage of being the standard implementation. So, the spec needs to do what they do so users don't get inconsistent behavior. Then, the spec work might find errors or validate proposals that can feed back into reference implementations. Finally, as with KCC, the implementation might be useful for looking into compiler errors or subversions.