Certainly a more practical conclusion should be "functional units should do one and only one thing, and that thing well"
Eh? I don't follow. How's that even remotely related to having structured blocks?
avoid obvious flow control at any language level lower than the language primitive which enables functional units". Otherwise you have trouble with if.
How's that? An if
construct is well understood when it comes to formal proofs, and it's a block with exactly one entry, and one exit point:
,---> then-block ---,
/ T \
pre ---> expression ---+ +---> post
\ F /
`---> else-block ---'