This was a great comment. The fact that new notations/representations (be that tests, simulations, formal methods, etc.) must justify their additional cognitiv

This was a great comment. The fact that new notations/representations (be that tests, simulations, formal methods, etc.) must justify their additional cognitive overhead is a great point. Aside from unit and integration tests, I think that substantial new notation/infrastructure is most justifiable when the second notation/setting allows you to model parts of the problem that can't be modeled in the original notation. Embedded software is a good example. Although there are some tools that allow you to model the physical system alongside the control software, typically the code is written in C and so there's no way of expressing very important aspects of the problem in the implementation language. So a second notation can help. For example, simulators and HiL setups for testing or things like https://github.com/LS-Lab/KeYmaeraX-release https://github.com/LS-Lab/KeYmaeraX-release for formal methods. Security is another good example. Typically code does not include an explicit threat model or explicit security properties, and these aspects of the problem are often scattered across the code and difficult to reason about. So being able to capture those things directly in a second notation can add a lot. For example, automatic vulnerbaility scaners for testing or https://tamarin-prover.github.io/ https://tamarin-prover.github.io/ for formal methods. Distributed/fault-tolerant systems are yet another example where it's very hard to state the thing you want to state in the implementation language. Netflix's chaos monkey comes to mind.