[joelellis]

The author explains in the twitter thread (french):

https://twitter.com/DMerigoux/status/1314531302079688709

> The difficulty arose from a constraint on the part of the DGFiP which did not wish to publish, for security reasons, part of the logic of the calculation corresponding to the "multiple liquidations" mechanism. Raphael and I recreated this unpublished part in a new DSL.

> The DGFiP also did not wish to publish its internal test sets. We therefore proceed to the creation of a completely random test set, from the unpublished content, in order to be able to reproduce the validation of Mlang outside the DGFiP.

> A little less than a year after the publication of https://blog.merigoux.ovh/en/2019/12/20/taxes-formal-proofs...., we therefore found a compromise allowing to respect both the 'source code publication obligation, and the security constraints of the DGFiP.

> By allowing us to go to its operating site and confidentially access the source code that it did not wish to publish, the DGFiP has enabled us to find alternative solutions that make the publication of the source code concrete and operational. .