This doesn't look much simpler to me, and I suspect the problem with this approach will wind up being incomplete or overconstrained specifications, rather than incorrect programs.

To use the language of the op, it will be composed of many discrete simple assertions that excruciatingly specify the output.