Catala is not at all about "proving the law" formally (I'm not even sure what it would mean?). It's about having a formal language to translate law into that both matches the way law is usually written ("default logic") and allows to make numerical computations on. This can typically be used to implement tax or benefits law so that it is way easier to check that the algorithm computing taxes/benefits is correct compared to the actual state of the art of using general purpose programming languages.
definition qualified_employee_discount
under condition is_property consequence
equals
if employee_discount >=
customer_price \* gross_profit_percentage
then customer_price \* gross_profit_percentage
else employee_discount
Dang, I wish all law was written like this instead of the purposefully obfuscated legalise of (lobbied) legislative lawyers meant to mislead people and slip in loopholes for their interest groups to profit of.
Clear legislature is definitely something every person in the world would benefit of - if the the country's administration would want that.
For me, a great advantage is that this system makes it far simpler to understand the impact of a change, say a multi-pronged bill incl millionaire taxes, energy subsidy changes etc.
I don’t know if they do it, but it allows proving properties of the law. For example, that the tax increases with income or that an exception doesn’t accidentally increase the tax paid.
If you're interested in this topic, I very warmly recommend the book You're not a rock by Mark Freeman. There are also episodes of podcasts around with interesting interventions from him.
The way I usually pitch the book is that Mark is not an MD, or a scientific expert on the topic, but he is a patient who's been through it, is very interested, and explains to you how it worked for him, and what he knows about the topic like a friend would. There are some mistakes, some things are a bit awkwardly explain, but the book is overall a tremendous read for anyone interested in anything dealing with anxiety, ocd, or more generally a mind too keen on spinning in a wheel.
I am of the opinion that async/await syntax for efficient embedded programming is one of the true revolutions of Rust -- and often overlooked. I gave a presentation about this very idea at a recent Rust meetup in Paris. The slides are there if some are interested (though admittedly not very explicit on their own): https://docs.google.com/presentation/d/e/2PACX-1vRT_ejw7Uza6...
> I ended up writing a small JavaScript function to maximize font size: it makes the text invisible (via CSS visibility: hidden), tries displaying the text at a very large size, and then tries successively smaller font sizes until it finds a size that lets all the text fit. It then makes the text visible again.
That would be a good application for dichotomic search if performance was ever a problem (I doubt it though).
More generally, having elements on a grid of different sizes should hopefully be much more easy once CSS masonry grid is available.
reply