My student Denis wrote a formal semantics for the French tax code, complete with Coq proof of soundness and SMT queries to uncover unfair tax hikes. PL for fiscal justice! https://blog.merigoux.ovh/en/2019/12/20/taxes-formal-proofs.html …
-
-
oh to live in such a country lol
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
-
-
I'm extremely surprised of that, too
-
OK, reading the article, it's not that can of formal encoding. It's an SMT encoding in Z3 with the goal to find inconsistencies (or edge cases of properties combination). And a formal specification of the M language used by the dgfip to encode taxe laws
Kraj razgovora
Novi razgovor -
Čini se da učitavanje traje već neko vrijeme.
Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.