That depends on what you mean by "getting the job done". If what you want is to write a reference description of a protocol for a paper, and make mathematical p

That depends on what you mean by "getting the job done". If what you want is to write a reference description of a protocol for a paper, and make mathematical proofs of the protocol's properties, that's one thing. (The weakest model of computation there means you'll spend less proof effort around your surroundings -- language, environment -- and more on the protocol, giving you less leeway for error). If you want to write a real-world implementation of the protocol, then the story is different, because the complexities of the real world are unavoidable. You will add complexity to your toolset, to deal with the aspects of the environment that you abstracted away in your paper. When we write proofs for papers about type systems, we use ultra-simple languages like some typed variants of lambda calculus, which are the simplest thing that gets the job done. But once the type properties are proved, no one is expected to write their real programs that way -- they are expected to replicate those properties in the real world instead.