For some reason it strikes me that we don't think of a potato plant as needing life lessons. I doubt anyone here has moral compunctions about leaf structure or starch formation. People seem much the same way to me. Another part of me does instinctively model the inner world of people as small deviations from my own. Other parts of me think that is quaint.

It appears to me that the sense of clairty imparted by wisdom often looks like mere rigidity when seen from the outside. I have little doubt that your particular wisdom has been hard-earned, and at the same time, I think it is hopelessly myopic. The thing that gets me is that this also almost surely applies to my own wisdom, which is why I distrust them implicitly.

I think the world is so vast and our exposure so limited such that any Life Wisdom is hopelessly doomed to be a horrible overfit on the particulars of an individual.

Keep growing your idiosyncratic leaves though. I also genuinely think they're beautiful.

https://en.wikipedia.org/wiki/A_Book_from_the_Sky

Notice that whatever your goals are, they don't automatically serve the interests and per concerns of all your employees. Are you now delusional, evil, ruled by greed?

Running a smooth operation mostly just makes for really boring news. You should perhaps factor in survivorship bias of narratives into your views of the world.

https://us.metamath.org/mpeuni/df-rdg.html

Essentially, it's just doing a lazy fixpoint a la Haskell's fix function. The definition is a little more general, though, to make it work for both transfinite and well-founded recursions as well.

This chashed out nicely in a sequence builder:

https://us.metamath.org/mpeuni/df-seq.html

which specializes to "normal" recursion.

Now you have my attention. I'd love to read about some of these trivia.

The historical emergence answers here are fine as far as they go, but they're a bit like saying that Linux is an OS developed by Linus to help him learn x86.

IMO 9front is an exposé of what an OS can look like when it's written for and by hackers with a focus on simplicity. The YouTube channel adventuresin9[0] parades some nice examples of what real world usage looks like.

For example, since everything is just a file, you tunnel traffic with a simple bind mount. Since everything is just text, small regexes suffice to route mouse clicks to UI actions. Since windows are just buffers, grepping history is grepping the window's text buffer; taking a screenshot is just cp-ing the window's draw buffer.

Oh, and 9front C diverges from the standard intentionally in some nice ways: evaluation of function args is sequenced, anonymous unions like

    struct {
      int a;
      union {
        uint i;
        int j;
      };
    }

[0]:https://www.youtube.com/channel/UC7qFfPYl0t8Cq7auyblZqxA

That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.

Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.

This statement itself predicades on a Platonic realist metaphysics! Indeed, what is the ideal against which things are judge right and wrong? I think the psychological roots of Enlightenment rationality run deep in the West, making it brutally hard to usurp.

That said, I think we can go a long way in this one case by just throwing out the "wrong" judement and laser focusing on the particulars of utility that science provides. One zoomed-out facet sees it as a collaborative effort as squeezing out repeatable processes, a la Popper et al.

Proofs of incompleteness theorems, the halting problem, Rice's theorem etc. all share a diagonalization structure. The keyword here is Lawvere's fixed-point theorem[0], but it's a bit of abstract nonsense, so here's a good accessible video on the topic[1].

I'm not sure the incompleteness theorems themselves are immediately and directly applicable to software development, but I find that having several examples of diagonaization proofs bouncing around in my head makes the Lawvere structure apparent. Since proofs are just programs, the pattern is surprisingly pervasive. Futamura projections are one incarnation, which is essentially how many interpreters end up providing "compilation" of programs into standalone binaries.

[0]:https://en.wikipedia.org/wiki/Lawvere%27s_fixed-point_theore...

[1]:https://www.youtube.com/watch?v=dwNxVpbEVcc

We define computable numbers to be Turing machines, lambda reduction processes, or whatever your favorite model of computation happens to be. If you don't like this kind of definition, then we need to talk philosophy of computation.

To decide equality, we let your machines clunk along until they both produce a result, which we then compare (using another machine). Hello Mr. Halting Problem. Specific programs are fine, but comparing against arbitrary classes of program is the bugger. This is why discontinuous functions cannot exist in a hardline computable analysis theory.

People sometimes describe me that way when I start asking unbridled questions. Personally, I find that I can activate this mode when trying to connect answers to some sense of life meaning and the myriad ways that unfolds. Many on the receiving end find the experience frustrating, though.

I think we get used to repeatable patterns more than develop comprehensive understanding. The former feels like accomplishment, while the later feels like perpetual confusion, IME.

They're well-known and have a simpler implementation, and we are familiar with their quirks. There is a giant body of useful knowledge built up around standard real analysis. That doesn't really exist if you insist on using only computable numbers.

The computables are also more fiddly in many ways. Because equality is undecidable, you can't have discontinuous functions, you need to carry around error epsilons all over the place, and we lose useful tools like the Heine-Borel theorem, I think.

Try proving some results in PDE theory, and I think you might change your mind.

In general, I find clarity in thinking of numbers as the system that implements them, rather than as platonic objects with individual reality. What does using Old Boring tech buy you over using Shiny New Thing?