That makes sense - I don't know if that's what the blog post was implying though. Ironically, this blog post could probably benefit from a few more details about what the meeting was supposed to achieve :)

I should have been clearer.

When I said that good leaders pay attention to things from the bottom-up, that doesn't mean they always know everything needed for any discussion. It just means they are able and keen to understand the low-level details when they matter, because they routinely look at such details in the projects that they're involved in.

Of course it's possible that this story is just told badly and the SVP already knew the technical details, in which case the blog post is a bit misleading.

> I need them to tell me what we're going to change, and it needs to be a BIG systemic change, not minutiae, which is where many engineers thrive.

How can one know if the engineers' proposed "BIG systemic change" is appropriate and complete, without knowing the details of the problem it is addressing?

Something about this feels wrong:

- If you trust them completely, you don't need to know what happens next either. Just trust them to do the right things, your leadership isn't required.

- If you don't trust them completely, how can you know if "what happens next" is appropriate without knowing the details?

Isn't this just reinforcing the idea that leadership doesn't need to have their feet on the ground?

The best leaders I've worked with were paying attention to things from the bottom-up as well as top-down.

> https://lichess.org/lwiPq9wB#48

When I go to that link it shows Black is winning with -1.9 eval at depth 32 with SF19 1MB NNUE! It looks like it got this evaluation from the cloud database.

- it teaches resiliency in bad situations.

- it teaches you to not be too harsh on yourself as a person. If you watch GMs playing online, they make bad mistakes all the time too - they're not godlike creatures who make no mistakes, far from it.

The flipside is that if you approach it the wrong way (I know I have at many points), it can have the opposite effects too.

To approach chess in a mentally healthy way was a long process for me. You need to get rid of your ego and be objective as much as possible when playing, or it will just make you sour - this in itself is a valuable lesson.

I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand.

The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be trusted, it gets checked by the compiler.

Is this also the case for Go's joseki? Or is any deviation easy to punish?

This way we get to see their project fail.

I don't know which one is worse.

I must be missing something here, inside joke or something in the title?

On the bright side, I suppose one mitigating factor is that renewable energy makes it less harmful to use energy to power A/C usage.