Some of the interpretations won't be correct without grounding them in old case law. That's the expensive part, in many jurisdictions, the official interpretations by the tax department are not free.
replyNice. Is the lean used to formalize formulas?
replySort of. The formulas for each line live in the form YAML I described above. The formulas are built out of a set of primitive operations that are defined in lean, with their properties proved there (non-negativity, monotonicity, etc.). There's also a lean evaluator that's run on compiled form data and cross checked with the typescript evaluator. (There's a lot more detail in the README.)
replyYou are one sick puppy. This is a brilliant idea.
reply