rssoconnor

Thanks for reminding me of CGP Grey's "This Video Will Make You Angry": https://youtu.be/rE3j_RHkqJc

Now I feel I should rewatch this video annually as a reminder to myself, or maybe monthly.

It's also a temporary anomaly as the moon has been moving and continues to move further away from the earth. See Lunar Recession.

I presume he is the same one who authored "Divine Proportions: Rational Trigonometry to Universal Geometry" (https://www.goodreads.com/book/show/791022.Divine_Proportion...) so I suspect he is not misquoted.

I actually quite liked "Divine Proportions". As far as I know Wildberger is eccentric, but not exactly a crackpot.

The book I was just reading says that the genes for MHC (Major Histocompatibility Complex) molecules are among the most diverse genes in the human population, with even the suggestion that people find others with different MHC genes than themselves more attractive.

Normal distributions are the maximum entropy distributions for a given mean and variance. Therefore, in accordance with the principle of maximum entropy, unless you have some reason to not pick a normal distribution (e.g. you know your values must be non-negative), you should be using a normal distribution.

These slides from Ralf Hinze were instrumental to my understanding of how to use late-binding to define objects in a functional language: https://www.cs.ox.ac.uk/people/ralf.hinze/talks/Open.pdf

I have the following file called oop.nix dated from that time.

    # Object Oriented Programming library for Nix
    # By Russell O'Connor in collaboration with David Cunningham.
    #
    # This library provides support for object oriented programming in Nix.
    # The library uses the following concepts.
    #
    # A *class* is an open recursive set.  An open recursive set is a function from
    # self to a set.  For example:
    #
    #     self : { x = 4; y = self.x + 1 }
    #
    # Technically an open recursive set is not recursive at all, however the function
    # is intended to be used to form a fixed point where self will be the resulting
    # set.
    #
    # An *object* is a value which is the fixed point of a class.  For example:
    #
    #    let class = self : { x = 4; y = self.x + 1; };
    #        object = class object; in
    #    object
    #
    # The value of this object is '{ x = 4; y = 5; }'.  The 'new' function in this
    # library takes a class and returns an object.
    #
    #     new (self : { x = 4; y = self. x + 1; });
    #
    # The 'new' function also adds an attribute called 'nixClass' that returns the
    # class that was originally used to define the object.
    #
    # The attributes of an object are sometimes called *methods*.
    #
    # Classes can be extended using the 'extend' function in this library.
    # the extend function takes a class and extension, and returns a new class.
    # An *extension* is a function from self and super to a set containing method
    # overrides.  The super argument provides access to methods prior to being
    # overloaded.  For example:
    #
    #    let class = self : { x = 4; y = self.x + 1; };
    #        subclass = extend class (self : super : { x = 5; y = super.y * self.x; });
    #    in new subclass
    #
    # denotes '{ x = 5; y = 30; nixClass = <LAMBDA>; }'.  30 equals (5 + 1) * 5).
    #
    # An extension can also omit the 'super' argument.
    #
    #    let class = self : { x = 4; y = self.x + 1; };
    #        subclass = extend class (self : { y = self.x + 5; });
    #    in new subclass
    #
    # denotes '{ x = 4; y = 9; nixClass = <LAMBDA>; }'.
    #
    # An extension can also omit both the 'self' and 'super' arguments.
    #
    #    let class = self : { x = 4; y = self.x + 1; };
    #        subclass = extend class { x = 3; };
    #    in new subclass
    #
    # denotes '{ x = 3; y = 4; nixClass = <LAMBDA>; }'.
    #
    # The 'newExtend' function is a composition of new and extend.  It takes a
    # class and and extension and returns an object which is an instance of the
    # class extended by the extension.
    
    rec {
      new = class :
        let instance = class instance // { nixClass = class; }; in instance;
    
      extend = class : extension : self :
        let super = class self; in super //
         (if builtins.isFunction extension
          then let extensionSelf = extension self; in
               if builtins.isFunction extensionSelf
               then extensionSelf super
               else extensionSelf
          else extension
         );
    
      newExtend = class : extension : new (extend class extension);
    }

In nix overlays, the names "final" and "prev" used to be called "self" and "super", owing to this OOP heritage, but people seemed to find those names confusing. Maybe you can still find old instances of the names "self" and "super" in places.

Dave Cunningham created jsonnet from some conversations I had with him about how Nix's lazy language allows one to make recursive references between parts of one's configuration in a declarative way. No need to order the evaluation beforehand.

Dave also designed a way of doing "object oriented" programming in Nix which eventually turned into what is now known as overlays.

P.S. I'm pretty sure jsonnet is Turing complete. Once you get any level of programming, it's very hard not to be Turing complete.

I worked on the Galois theory needed in the formalization of the Odd Order Theorem. I wanted to check to see if I had this lemma. It's been over a decade but I think I found it: https://github.com/math-comp/math-comp/blob/84cb21e7bb853041...

    Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).

This says for intermediate fields K and E (within some ambient separable (finite dimensional) field extension L / F), 'Gal(E / K), the group of automorphisms of E that fix K†, conjugated by (written as :^ ) x‡ is equal to 'Gal(E / x @: K),the group of automorphisms of E that fix x @: K which denotes x(K).

The fields E K and F in this proof correspond to the fields L M and K from the article; 'Gal(E / X) corresponds to X* from the article; and of course x corresponds to τ from the article.

†) technically that fix E ∩ K since our notation doesn't technically assume that K ≤ E.

‡) I believe by type inference x must be something we can conjugate the group by, and thus is must be a generic automorphism of E, i.e. an F-automorphism of E.

Can you use the spare electricity to stockpile some sodium hydroxide or something?

Due to way the Chinese government operates in other countries, if you happen to be ethnically Chinese living in the West, the Chinese government is still probably more of a threat to you than Western governments.

https://www.cbc.ca/news/canada/ottawa/rcmp-chinese-police-st...

I do think the why that the Four Colour Theorem is true is captured my statement. The reason why it is true is because there exists some finite unavoidable and reducible set of configurations.

I'm fairly sure that people are only getting hung up on the size of this finite set, for no good reason. I suspect that if the size of this finite set were 2, instead of 633, and you could draw these unavoidable configuration on the chalk board, and easily illustrate that both of them are reducible, everyone would be saying "ah yes, the four colour theorem, such an elegant proof!"

Yet, whether the finite set were of size 2 or size 633, the fundamental insight would be identical: there exists some finite unavoidable and reducible set of configurations.

Is the proof of the Four Colour Theorem really that unsatisfying?

The Four Colour Theorem is true because there exists a finite set of unavoidable yet reducible configurations. QED.

To verify this computational fact one uses a (very) glorified pocket calculator.

I figured the carbon tax just needed to reach $100-$200ish per tonne, because that is the quoted price to scrub CO2 from stacks.

Ah yes, I see what you are getting at.

But to clarify the report's indirect costs is not due to (just) indirect costs on buying goods transported by carbon tax, but the report's additional "economic factors" is due to "the loss in employment and investment income".

But I personally find this take in their report unfair because the the alternative of not having the carbon tax isn't really the status quo, because there is an "economic cost" from climate change such as 'the interior of BC being hotter than death valley' and 'the town of Jasper burning down'.

That said, I do see that I'm rationalizing my personal beliefs on this topic, and that is also unfair.

FWIW, I got a combo washer dryer, specifically this one https://youtu.be/x44YAiVCbAY (not my video), because I don't have a dryer vent.

While it was a pretty big upfront cost, the combo does have the advantage of entirely reimagining how one does laundry! Specifically because it both washes and dries you can just run it overnight and in the morning you take out dry clothes. So no more laundry days; every night is a potential laundry night. Not only is it energy efficient, it also runs on my ultra-low overnight time of day rates, because that is simply the most convenient time of day to run it anyways.

I think the above video review covers basically everything. I do agree the clothes do not come out super dry, and sometimes I do run it a little longer, or let things air out a bit. Clothes are usually fine and sheets are slightly less fine. Also there is no lint trap, so I have to keep wiping out the lint.

Overall I think the advantages outweigh the disadvantages with not having to babysit the washing machine ensure wet clothes are transferred to the dryer in a timely fashion.

Can you explain what you mean by making every[one?] noticeably poorer when they have most to all of their payment reimbursed? (for the median individual it is more like "all to more" since the carbon credit is not capped at one's individual carbon tax payments)

> But the case was thrown out in August 2023 — not for a lack of evidence, but because the Crown took too long to bring it to trial under a set of strict timelines that have reshaped the way criminal cases are handled since a landmark 2016 ruling by the Supreme Court of Canada.

https://www.cbc.ca/news/canada/british-columbia/canada-jorda...

Can someone draw what hinkley is talking about?

> can I solve this with Syncthing?

I recently found out that Syncthing is ending Android support. :(

I'll repeat my comment from last time this came up.[0]

I could be wrong (and I probably am) but I feel like the term "reproducible build" has shifted/solidified since 2006 when Dolstra's thesis was first written (which itself doesn't really use that term all that much). As evidence the first wikipedia page on "Reproducible builds" seems to have appeared in 2016, a decade after Dolstra's thesis, and even that stub from 2016 appears to prefer to use the term "Deterministic compilation".

Anyhow, when the Nix project originally spoke about "reproducible builds", what I understood was meant by that term was "being able to repeat the same build steps with the same inputs". Because of the lack of determinstic compilation, this doesn't always yield bit-by-bit identical outputs, but are simply presumed to be "functionally identical". There is, of course, no reason to believe that they will necessarily be functionally identical, but it is what developers take for granted every day, and if otherwise would be considered a bug somewhere in the package.

With Nix, when some software "doesn't work for me, but works for you", we can indeed recursively compare the nix derivation files locating and eliminating potential differences, a debugging process I have used on occasion.

I agree that "reproducible builds" now means something different, but that isn't exactly the fault of Nix advocates. I guess a new term for "being able to repeat the same build steps with the same inputs" is needed.

[0]https://news.ycombinator.com/item?id=41953155

I literally blog with raw SGML. Each post comes with a handful per post ENTITYs for that post's common abbreviations and links. Unlike inopinatus's comment, I do keep up with "modern" standards, which is why my posts conform to the "ISO/IEC 15445:2000//DTD HyperText Markup Language//EN" doctype, the latest HTML standard approved by the ISO.

Blog content is assembled via various SGML entities includes into a prehtml file of "-//ISO-HTML User's Guide//DTD ISO-HTML Preparation//EN" doctype per ISO 15445:2000 recommendations[0]. This is all processed with osgmlnorm through a somewhat simple Makefile to generate the resulting HTML files.

[0] https://rogerprice.org/15445/UG.html#DOCPREP

I was reading about the Order of Cistercians the other day, and I am reminded of this passage from wikipedia:

Relaxations were gradually introduced into Cistercian life with regard to diet and simplicity of life. Also, they began accepting the traditional sources of income that monks in comparable orders used: like rents, tolls, and benefices. The agricultural operations were blessed by success. Wealth and splendour characterized the monasteries, so that by 1300, the standard of living in most abbeys was comparable, if not higher, than the standards middling nobles enjoyed.[59]

[59] Jaritz, Gerhard (1985). "The Standard of Living in German and Austrian Cistercian Monasteries of the Late Middle Ages". In Elder, E. Rozanne (ed.). Goad and Nail. Studies in medieval Cistercian history. Kalamazoo, Michigan: Cistercian Publications. p. 57. ISBN 978-0-87907-984-0. "A study [Watzl 1978] done for the Lower-Austrian abbey of Heiligenkreuz demonstrates that in the first half of the fifteenth century, no fewer than 201-207 days of the year saw extra food."

I get what you are saying. My point is that someone who is philosophically disinclined to buy into the "existance" of non-computable real numbers, e.g. constructivists, because they are not effectively computable, are also going to be, by the same logic, disinclined to buy into your argument that the computable real numbers are countable, because in order to count the computable real numbers you would need a function to enumerate them, at that function is also not computable.

> But the set of programs that compute real numbers is a subset of all programs, and the set of all programs is countable. Therefore the set of computable numbers is countable.

A constructivist is also not going to buy into your argument that a subset of a countable set is countable. Heck, the constructivists are not even going to buy into an argument that a subset of a finite set is necessarily finite (they have a term for such subsets: 'subfinite').

Yes, I know that this constructivism feels so bizarre that it cannot possible be coherent; the whole notion of cardinality appears to become useless. But you get used to it after a while.

Heck, even in classical mathematics, trichotomy of cardinally requires (or rather /is/) the axiom of choice. So cardinality wasn't really super well behaved to begin with.

As a constructivist, I somewhat agree with your viewpoint, though my views are a bit more nuanced. (e.g. Dedekind's construction of the continuum as a collection of points is perhaps the primary source of corrupted thinking, which muddles even well-meaning thinkers into thinking that it is even possible to separate computable points from non-computable points. The real numbers form a /continuum/, and a continuum cannot be described as simply a collection of points.)

That said I believe your comments are off the mark in regards to the topic of the Weierstrass function. The Weierstrass function is completely well behaved from a constructive point of view[0]; it is uniformly continuous and everything. In particular we can (constructively) map (constructive) real numbers to (constructive) real numbers via this function.

[0]https://mathoverflow.net/a/43904

It is not /really/ countable in a computable sense; it is undecidable whether or not a program generates a real number or diverges (as a consequence of Rice's theorem). Thus you cannot compute a function that enumerates all programs that compute real numbers.

It has been my experience that if the ICE engine in the Prius Prime switches on for the first time for any reason, it prefers to remain on for several minutes at a minimum, no matter what. I have a theory for why this happens, but it is purely speculation on my part.

I’d much prefer to smell a car coming than not, personally.

> None of that would have mattered that much, but the dealbreaker: Trunk space.

I hear you. I got a 2022 Prius Prime and I was disappointed with the smaller trunk space compared with the 2010(ish) Prius I had before, but I still went with it. However, my understanding is that the newer models somehow have even smaller trunk space space. At least that space under the trunk floor is filled with batteries in my case.

While I'm happy enough with my purchase, I suspect I won't be getting a Prius in the future. If I want a PHEV, I might look at the Rav4 Prime, but I think I'm more likely to look for a full EV when the time comes.

> - No way to defrost your windshield, unless you're already driving

I have a 2022 Prius Prime, and I am moderately sure with the car on and in park I can press the front window defrost button, and the ICE will turn on and start blowing hot air on the front window.

Also, while parked and plugged in at home, I can use the remote A/C button to start heating the cabin and front windshield while clearing off snow and clearing the driveway, and will be powered from my house. I'm not sure if this also works without being plugged in.