Viewing profile — xelxebar

Pretend for a second that you're in a position of trying to run a successful business. Congrats, you're a c-suite executive now. Of course, you are free to define "successful" by w…

Hurd specifically includes a userspace. Its kernel is Mach.

Intriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function: https://us.metamath.org/mpeuni/df-rdg.html Essentially, it'…

> I can remember some obscure AIX partitioning-related fact Now you have my attention. I'd love to read about some of these trivia.

I daily drive 9front. 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. …

Ease of implementation means we get more, independent verifiers rather than trusting any particular one.

I would expect proofs that exploit kernel bugs to look fishy, so someone reading the proof could catch the smell. That said, I'm sure there's also room for underhanded Lean program…

That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you…

If you take seriously the notion that enlightenment isn't some separate state or goal to be reached but simply the actualization of things as they are, I find the goal- and outcome…

> The thing is, we are wrong, but this stuff is useful to make predictions. This statement itself predicades on a Platonic realist metaphysics! Indeed, what is the ideal against wh…

Geocentric coordinates are easily observable; just look at the sunrise and sunset. And if you zoom out even more and look at the galaxy, heliocentric coordinates become unreasonabl…

Yeah, that github URL should be fixed. The HOL database is here https://github.com/metamath/set.mm/blob/develop/hol.mm

Hallucinations like these make it pretty clear that these agents do not really understand or think, IMHO.

Programs as data. Proofs of incompleteness theorems, the halting problem, Rice's theorem etc. all share a diagonalization structure. The keyword here is Lawvere's fixed-point theor…

Okay, theorem=generalized-continuum hypothesis. If you use exotic axioms to give that a definite result, the go eat a Gödel. We define computable numbers to be Turing machines, lam…

Has anyone here found ways to actively cultivate this kind relentless curiosity within themselves? People sometimes describe me that way when I start asking unbridled questions. Pe…

> What do "real" numbers buy you? 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 ar…

Better yet, git reset ORIG_HEAD or whatever is usually sufficient[0]. The reflog is the general solution, but git's magic references do provide quite a few niceties. https://www.ma…

Does this not do what you want? git rebase -i master..HEAD The gitrevisions(7) manpage is a good reference to keep in your back pocket, I find. https://www.man7.org/linux/man-pages…

Using ordinals to talk about finite numbers gets suprisingly deep real fast. David Metzler has a series of fun videos called "Ridiculously huge numbers" that goes down the rabbit h…

Considering incentive structures at play is solid epistemiology, but the line of thinking in your comment is a tad reductive, IMHO. In the hypothetical world where 1 is true, what …

Interesting. "A is X" is different than "I experience X from A". The former employs an objectivist lens while the latter a subjectivist one. I have had the pleasure of witnessing d…

9front is a fork of Plan 9, the operating system that runs Jurassic Park[0]. Stanley Leiber is a prominent contributor, albeit whose existence is humourously-but-seriously-maybe de…