The name “bool expression” is rather unfortunate, since it is usually reserved for “an expression of type Bool”. What is discribed here is really propositions, i.e. “Prop”.

Prop is fundamentally different from Bool in Lean and all the language I know. For lean in particular, Prop is defined as a complete lattice, yet Bool is only inhabited by True and False (ignoring incomputable etc). More intuitively, Bool require all the true (or false) statements to be collapsed into a single value true (or false); yet for Prop, provable statements are not necessarily equal to each other.

But I really enjoyed the analogy between expressions that returns bool in other languages and leans prop, seem like a great starting point for people.

Linus have stated multiple times that he does not break user space, thus this quiet clearly cannot be real.

I heard in many large companies, they would create short artificial downtime for internal services, so that user-facing system never rely on a single internal system for resources and data. This prevents large downtime in user facing system when any internal service is down for a large amount of time.

I think a great use of interns is to make these downtime more organic.

Engineers can laterally move to more prestigious or challenging projects if they prove worthy based on their skills and connections. One former staffer tells WIRED that this made the company feel like a meritocracy where the best people, and the best ideas, naturally rise to the top.

I am very interested in the culture and psychology of these supposed “meritocratic” companies. Personally, I don’t believe we have a reasonable approximation of the hyper-efficient merit-based resource allocation that is promoted by the ultra-rich.

Usually I find these so-called “meritocratic” policies do not encourage good ideas, but enable hyper-competitive environments.

These kind of environments likely do not support solid well-thought-out proposals; instead, pushes the quick implementation of mediocre ideas (a.k.a move fast and break things). A hyper-competitive environment can also discourage collaboration, which often can be crucial to “solve the hard problems”.

And the article mentions that this environment boosts employee retention, which I find extremely interesting. I wonder if the constant competitions can keep triggering a sense of “winning” and “accomplishment” in a perhaps mundane job.

Secureboot is a security measure to make sure the boot environment have not been tampered with. It would detect malwares that attempt to modify the boot environments. According to ArchWiki, it ensures “core boot components (boot manager, kernel, initramfs) have not been tampered with”, which would protect against initramfs-swap attacks like de-LUKS, however there are conflicting reports on the internet, and I have not tried myself.

I personally don’t find it makes Linux harder to install, like others suggested. Unless you use a surface device, it will happily accept the key for most common linux distro, including Ubuntu, Debian, Fedora, and many more. For most custom distros, you can easily register its key via MOK (require root privilege and confirmation in the UEFI, for security purpose). In fact, Debian project is quite clear on SecureBoot not being a tool for MS to monopolize the desktop market: https://wiki.debian.org/SecureBoot#What_is_UEFI_Secure_Boot_NOT.3F .

However, if you need to load additional kernel modules, like NVIDIA drivers, secureboot can get quite annoying. I am actually quite interested in why Windows don’t have a problem loading additional drivers, yet Linux do.

In the end, I feel if you are using a distro that works with secureboot, there is no reason to leave it off; if you find it annoying, yet okay with a downgrade in security, then you might want to leave it off.

This face is as excited as a cat can get.

I am in this picture and I don’t like it.

It seems like they have replied and said they won’t repel the act.

Unfortunately, even EU’s solution doesn’t support non-google-backed android.

It feels very strange to me that any serious citation counter would index ResearchGate, which AFAIK don’t have any check before publishing a preprint. It is basically a more reputable vixra.

But then again citation count, or “impact factor”, are in general quite bad to determine the quality of one’s research, and often can be easily manipulated even through legitimist means: simply publish more mediocre papers.

This is actually gaming the Google Scholar system instead of harmless ones like Willard.

https://www.science.org/content/article/how-easy-it-fudge-your-scientific-rank-meet-larry-world-s-most-cited-cat

Give it another 20 years, PHP might even evolve to catch up with programming languages in the 1980s 😮

I think she played a lesbian 20 years ago in a comedy TV show. I don’t know if it is fair to call it “porn” https://teletubbies.fandom.com/wiki/Pui_Fan_Lee

Yes, you are right, topologists’ sine curve includes the origin point, which is connected but not path connected. I guess I didn’t do very well in my point-set topology. I will change that in my answer :)

Sure, I have no problem with analogy. I called them lie simply to peak people’s interest, but in research and teaching, lies can often be beneficial. One of my favorite quote (I believe from Mikołaj Bojańczyk) is “in order to tell a good story, sometime you have to tell some lies”.

At the begining of undergrad, “not lifting pen” is clearly a good enough analogy to convey intuition, and it is close enough approximation that it shouldn’t matter until much later in math. I can say “sin(1/x) is a continuous function on (0,1] but its graph is not path connected”, which is more formal, but likely not mean anything to most of the reader. In that sense, I guess I have also lied :)

However, I like to push back on the assumption that, in the context of teaching continuous function, the underlying space needs to be bounded: one of the first continuous function student would encounter is the identity function on real, which has both a infinite domain and range.

The second one is the cantor function, also known as devil’s staircase; the third one is topologist’s sine curve.

Functions on real numbers are incredibly werid.

There are continuous but nowhere differentiable functions.

There are continuous and monotonically increasing function that goes from 0 to 1 (i.e. surjective function [0,1] →[0,1]), that “almost never” increases; specifically, if you pick a point at random, that point will be flat on said function with probablity exactly 1 (not almost 1, but exactly 1, no approximation here).

More impressively, you can have function that is continuous, but you cannot find a connected path on it (i.e. not path connected). In plain word, if anyone told you “a function is continuous when you can draw it without lifting your pen”. They have lied to you.

EDIT: the last one (crossed out) is wrong. Intuitively “topologists’ sine curve” contains two parts; you can neither find a distinct seperation for them (i.e. “connected”), nor can you draw a path that connects the two part (i.e. not “path connected”). However, topologist’s sine curve is not the graph of a continuous function.

Yeah, a lot of time I don’t know if I am just fine or too tired to feel anything…

TO THE UK GOVERNMENT

Gay Oedipus