> 1. It would not, the tax law remains the spec.

Unless you rewrite the law to make the code the spec. Indeed, code is probably a better medium for unambiguously communicating calculations.

> 2. France does provide an executable encoding of the tax code, TFA is literally a compiler for that.

But other countries might not do so.

> 4. You can use OpenFisca to encode your own country's tax law, or lobby for your country to encode its tax law there (https://openfisca.org/en/packages/).

This would be amazing!