Hacker Newsnew | past | comments | ask | show | jobs | submit | igravious's commentslogin

Should not Is that your new law? The non-agentic “Neovim and Zed *never tried to sign commits [for]~~with~~ me” therefore no tool ever no matter how advanced is not allowed to sign a commit.

Did it ever occur to you that for whatever reason you just might not be cut out for the software treadmill?


> > a set can contain itself

> Can it?

Yes -- in set theory sets can contain themselves

> > a term can have only one type... Due to this law, types cannot contain themselves

> Doesn't look like one follows from the other...

types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them


> Yes -- in set theory sets can contain themselves

Which set theory? ZFC doesn't permit this.

Non-well-founded set theories are so non-standard that I think it's wrong, or at least misleading, to claim that unqualified "set theory" permits this.


> Yes -- in set theory sets can contain themselves

Hrbacek and Jech would like a word. It is very much not the case that in standard axiomatic set theory sets can contain themselves, precisely because this leads to things like Russell’s paradox. Sets containing themselves is generally prevented by the axiom of regularity. (Every non-empty set S contains an element wihch is disjoint from S) https://en.wikipedia.org/wiki/Axiom_of_regularity

> types are not sets and sets are not types

This is also not true. All types can be expressed as sets but not all sets are types in the standard definitions.


to justify my claim with an excerpt from the article:

““ What is type theory

    “Every propositional function φ(x)—so it is contended—has, in addition to its range of truth, a range of significance, i.e. a range within which x must lie if φ(x) is to be a proposition at all, whether true or false. This is the first point in the theory of types; the second point is that ranges of significance form types, i.e. if x belongs to the range of significance of φ(x), then there is a class of objects, the type of x, all of which must also belong to the range of significance of φ(x)” — Bertrand Russell - Principles of Mathematics
In the last section, we almost fell in the trap of explaining types as something that are “like sets, but… “ (e.g. they are like sets, but a term can only be a member of one type). However, while it may be technically true, any such explanation would not be at all appropriate, as, while types started as alternative to sets, they actually ended up being quite different. So, thinking in terms of sets won’t get you far. Indeed, if we take the proverbial set theorist from the previous section, and ask them about types, their truthful response would have to be:

    “Have you seen a set? Well, it has nothing to do with it.” [<=== important bit] 
So let’s see how we define a type theory in its own right. ””

The modern formulation of functions as sets doesn’t require type theory but is entirely congruent with Russell’s definition, just much less cumbersome. In this view, φ is a relation on the set (D X C) where D and C are the domain and codomain of the function (which he calls the “range of significance of x” and the “range of significance of φ(x)” respectively). So since he’s talking about propositional functions, here C is the set {true, false} and D is all the things that are like whatever x is ie the set {x’: x’ is of the same type as x}.

Now a relation is just a particular type of predicate (ie it too is a set) so here we have x ~ y if φ(x) = y for all (x,y) in (D X C).

Notice here both the propositional function and the type are sets.


Oof. If sets and types aren't the same, then sets and barbers are definitely not the same!

TFA is right. Parent comment is not really rebutting in any meaningful way. Your rebuttal makes less sense.

>> "a term can have only one type... Due to this law, types cannot contain themselves"

> types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them


> in the way you are linking them

This is what the text says, not me.


demonic

deceitful

despicably detrimental

DR-DOS was more than alright, if Microsoft hadn't smothered it the computing world would look very very different today …

I'm sure this is a mostly forgotten part of computing lore; apologies for the Gemini's Overview:

“Microsoft actively stifled DR-DOS in the early 1990s through anti-competitive tactics, primarily using the "AARD code" in Windows 3.1, which deliberately created compatibility errors to scare users away from the competing operating system. Microsoft also used FUD (fear, uncertainty, and doubt) tactics, such as hinting at future incompatibilities.

Key Tactics Used by Microsoft:

    The AARD Code: Windows 3.1 installer contained heavily obfuscated code, discovered in 1992, that specifically checked if the system was running DR-DOS. If detected, it displayed a fake "Non-Fatal Error" message to induce panic.

    Vaporware Announcements: Microsoft announced upcoming versions of MS-DOS to dampen demand for current versions of DR-DOS.

    OEM Pressure: Microsoft leveraged its monopoly to ensure pre-installed Windows came with MS-DOS, hindering DR-DOS's retail market success.
While Digital Research released a patch (the "business update") to bypass the AARD code, the damage to market perception and OEM deals was significant. The case was later part of legal battles between Caldera (which acquired DR-DOS) and Microsoft.”

https://share.google/aimode/JJs7wliOGtvnme6LY” [Tech Monitor/Wikipedia]


> Don't post generated comments or AI-edited comments. HN is for conversation between humans.

https://news.ycombinator.com/newsguidelines.html

Your comment would have been just as interesting as the first line followed by a link to https://en.wikipedia.org/wiki/AARD_code .


Yeah we know of the issues, and related lawsuits, and here we are OEMs still only sell GNU/Linux devices on their online shops, leaving to regular consumer stores Android, WebOS and Chromebooks.

Ah, and Valve had to come up with Proton, as game studios can't be bothered to natively target GNU/Linux.



Flagged as advertisement


What advertisement?

Codeweavers is literally the company behind Wine. Without them project would never reach point where it is now.

Codeweavers developers historically been authors of 2/3 (and likely even more in past) commits in Wine.


Uh?

CodeWeavers : Wine :: IBM/RedHat : Fedora


“And because Proton, SteamOS, and every downstream project builds on top of Wine, those gains trickle down to everyone.”

the gains would trickle up, no?


Driver issues are way more of a thing on Windows than Linux or MacOS.


Getting hardware to work is MUCH harder on Linux


It depends. For a lot of hardware it's actually easier to get working on linux, because the driver is just part of the kernel and you don't have to do anything special, including manually installing drivers, to get it working.

There are some cases where hardware support on Linux is suboptimal, such as Nvidia cards and many fingerprint readers, but things are a LOT better now than they used to be. Most consumer laptops and desktops will run linux just fine.


Last years I have had more problem with hardware in windows than in linux. It is not so trivial anymore.


Please provide examples.


In 2022 we got new zen 5 amd cpus almost when they came out, windows did not recognize a bunch of stuff and had to find and download individual drivers. In linux (ubuntu) everything worked out of the box, except only that the LTS release did not support the kernel that supported the new mobos yet and had to install the rolling release instead.


Please provide examples.


Correct again -- CC- applies to data, not code -- weights are data, open weights suggests a creative commons approach …

“ CC-BY 4.0 Creative Commons Attribution 4.0 International

This license requires that reusers give credit to the creator. It allows reusers to distribute, remix, adapt, and build upon the material in any medium or format, even for commercial purposes.

BY Credit must be given to you, the creator. ”

it's annoying the open source term is being cargo-culted around and I hate to say it but that ship looks like it has sailed.

funny that free software people were infuriated by the open source term and now the open source term is being completely misused in another context


Correct. (and I know you already know this but just for the record: (Nearly?) Everybody abuses the term "open source" when it comes to models. OSI have a post about it: https://opensource.org/ai/open-weights


“Oil and gas prices jump after US-proxy Israel attacks Iranian gasfield infrastructure, and after Iran responds in kind after having promised to do so.”

is a headline that reflects reality and doesn't finesse the details -- I should really become a headline writer, I'm clearly better than whoever is employed by The Guardian.

At the very least it should be "Oil and gas prices jump after Israel and then Iran attack gasfields"

Putting Iran first might lead some to believe this was Iran-initiated, which of course is probably the intention.


is israel a US proxy? that's feeling a little backward right now.


all proxies do this eventually.

no one ever seems to learn, you use a proxy to do dodgy shit for you and eventually they become the tail that wags the dog.

made worse in this case by the fact that trump is a weak leader and Netanyahu is not.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: