[nickpsecurity]

CakeML, a Standard ML subset, can compile to ASM with mathematical proof of correctness. You know your ASM will be what you expected it to be. There's also tools like QuickCheck, QuickSpec, and SPARK that can automate lots of analysis. Tons of work like this in compilers and static analysis with smart people always improving them.

Good chance your business logic will not be handled that well. So, good to structure it in a way to facilitate easy analysis or optimization by tools that currently exist or are in development. You get long-term benefits.