I'm glad more people are seeing just how applicable lean is to use cases beyond conventional theorem proving and math
I've been working on a project that involves generating monomorphized Rust based on lean specifications and the grind tactic works surprisingly well as an optimizer for stuff like pushdown
Searching a simple model of the Roth IRA for the known backdoors is a good tutorial example. Surprisingly the article just ends there instead of repeating the analysis on the rest of US tax law to find any novel loopholes.
The problem you'll run into with nearly all "loopholes" in administrative law (of which tax is one fairly thoroughly legislated and litigated variety) is that you'll get something that hinges on some administrative interpretation of something that "should" go your way based on transitive logic but when you try and get them to do that they'll just dig in their heels and say "sue us" knowing full well that it's more than it's worth.
5 comments
[ 6.8 ms ] story [ 12.4 ms ] threadI've been working on a project that involves generating monomorphized Rust based on lean specifications and the grind tactic works surprisingly well as an optimizer for stuff like pushdown