The hard part would be designing a machine-readable and illiterate-writable language for formal specification of Excel spreadsheet requirements to validate agai

The hard part would be designing a machine-readable and illiterate-writable language for formal specification of Excel spreadsheet requirements to validate against. And getting said illiterates to use it. There is no other way to detect errors involving somebody using SUM instead of AVG or aggregating data from wrong fields (examples from the article).