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 …
-
-
Interesting stuff, over a decade ago I was involved in a working group that tried to do a formal spec for the dutch tax authorities (in Coq as well). They were very interested, might be good time to follow up on this. Is there a recording of the presentation? Also:pic.twitter.com/gO8vTlQI77
Hvala. Twitter će to iskoristiti za poboljšanje vaše vremenske crte. PoništiPoništi
-
Č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.