whoke

4 ms·

1. 1.▲
   by whoke 2mo ago

   I like the concept of "inevitable grittiness"! I think languages like Lean actually do a very nice job of pushing the grittiness out to the boundaries of your program. Everything else can stay pure, and in domains that are amenabl
2. 2.▲
   by whoke 3mo ago

   I'd say this is relative to the novelty of the problem domain. At work I'm often solving problems that have fairly standard solutions, e.g. Python scripts to automate build and execution workflows. For this stuff I'm often ha
3. 3.▲
   by whoke 3mo ago

   "you haven’t done any of the hard thinking you would normally do in writing the code yourself" It's true, I spend less time solving problems that arise naturally from the process of implementation. But implementation errors h
4. 4.▲
   by whoke 3mo ago

   I think the interesting part here is that the black box gives us a starting point. And it's not a true black box: if a model is generating Lean, we can examine the entire source, iteratively refine by refactoring into smaller self-cont