after meditating regularly for a while, doing a noting practice produced a distinct shift for me on this point. I realized that most of the time, when I hear a sound there is also a momentary "shred" of visual/muscular thought that accompanies it. for example, when I hear a crow, there is a bit of black/feathery/tree-branch/etc. if this is interesting, you can find instructions from Shinzen Young online.
typing this up, I realize I'm not totally sure to what extent this is something that was happening before the practice vs something that developed from it [i.e. less habitual energy spent blocking things out], but either way I recommend it :)
attempt to interpret the parent comment more charitably: when different people who've shared a common experience try to put it into words, there is some consistency between what they write. the harder the experience is to verbalize, the harder it is to come up with meaningfully different precise descriptions of it, and the more aware you are of the limitations of language
personally, the post resonates strongly. focusing on this way of seeing has improved my life tremendously.
based on the very little I know of you (your two posts) it sounds possible that the point isn’t landing. you seem to be living near the “control = safety/happiness” realm, where the high order bit of life is controllability.
try reading it again, and notice how little specific advice is given towards how to cultivate the sort of attention he’s pointing at (maybe his most concrete advice is in the form of a painting of an owl).
are you convinced that by trying hard enough the future can belong to you, or that life owes you something? you can create an arbitrary amount of suffering for yourself by living that delusion (or the opposite one, that you can’t influence anything).
the notion expressed in the post is really worth trying, and simple, but hard to explain.
one idea: the next time you see something you personally find beautiful (a flower, the sky? the fact that the earth supports you effortlessly?) you could investigate whether you did anything to “deserve” that.
it points out that the bit complexity of the traditional algorithm is actually quadratic. and apparently, restricted to fixed width integers, there is a constant time method.
that is a neat demo with a lot of useful links! In fact, it seems that the Lean developers/community are very interested in new methods of achieving readability, and providing users with tools to build interfaces that scale up to the complexity of real workflows.
(at that timestamp, there's a quick introduction to their typical use at the moment).
lean4 is committed to all sorts of extensibility; here's a demonstration of the new macros: https://twitter.com/derKha/status/1354082976456441861. There have also been several instances of users implementing old lean3 features (for example, the `calc` tactic mode, which has unique syntax for proving (in)equalities) by simply defining new type classes and short macros.
> My main idea is that as a programmer what I do is constantly reducing the set of all programs to a particular program which satisfies the specification.
An alternate point of view is to start with the specification, interpreted as a generally nondeterministic program, and then refine it using logically sound optimizations to render it executable. This is roughly the approach of Fiat: http://adam.chlipala.net/papers/FiatSNAPL17/
typing this up, I realize I'm not totally sure to what extent this is something that was happening before the practice vs something that developed from it [i.e. less habitual energy spent blocking things out], but either way I recommend it :)