When you are reading a book, you certainly need to use your attention. However, you stay in a given topic/world for a sustained amount of time. This feels very different and much less tiring than scrolling on your phone jumping from topic to topic. Especially social media feeds that have been optimized to keep using it as long as possible (dopamine hits and all).
Newspapers are probably an intermediate between those two, to various degrees depending on the specific newspaper (trash vs deeper analysis).
That's great if it works. But it's way harder to produce a formal proof. So my expectation is that this will fail for most difficult problems, even when the non-formal proof is correct.
Even if they take the same number of ticks, shouldn't xor fundamentally needing less work also mean it can be performed while drawing less power/heating less, which is just as much an improvement in the long run?
Your city/rural distinction is insightful. I think it can be taken into account relatively easily. Name explicitly the cities/locations were the requirement would apply. Possibly based on some objective criteria like population density.
Not sure about the legal frameworks in the US but that’s exactly how it works in most places in the UK. Cities have restrictions for on-street parking (metered, permitted, illegal) whereas the towns and villages don’t (unless they also bring in bylaws to help with congestion).
In the US it varies a lot based on what state you're in. Some states give the cities a wide latitude for such policies, but some states (notably 'red' ones where the state government is likely to be conservative and the cities are likely to be liberal) do not grant cities the flexibility to make ordinances like this.
If you're not doing code review, you're not doing code review. If you're not gating builds on code review, you're not doing code review. If your developers are lazy and just approve the PRs as they land, you're not doing code review.
If you're thinking there is some magical line where LOC < n gets properly reviewed, but LOC > n doesn't, I assure you that's not the case.
And no one is turning off their approval gates in their build pipeline just to accommodate AI code.
> obviously no one’s running any compiled Lean code in any kind of production hot path
Ignorant question: why not? Is there an unacceptable performance penalty? And what's the recommended way in that case to make use of proven Lean code in production that keeps the same guarantees?
You’re right, there is that one example. Feels like we’re in exception that proves the rule territory. But I’d be very interested in being proven wrong! This isn’t a desire of mine, just what I’ve seen. Do you have other examples?
Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.
> Digital:
> [...]
> 6) of or relating to the fingers or toes. Ex: digital dexterity
reply