It's hard to say who will fare best, but it's evident who'll do the worst. The European Union will regulate AGI out of existence. Most citizens would not want to use it because of climate change, or something.
I think poor countries with weak democracies or dysfunctional systems would do pretty good with AGI. I don't believe democracy will survive AGI, except, perhaps in the United States.
It is all fun and games, until people figure out that intelligence, has nothing to do with morality and what is good or bad.
Being run by AGI can be an utopia, or AGI will become pure eugenics state - Why are we keeping elderly or handicapped people alive? Waste of resources, terminate them. Why are we allowing something like love to exist? People should be selected for breeding based on <trait which AGI considers important>
Add to AGI superior intelligence and very likely an ability to manipulate humans, then people will wholeheartedly agree with whatever nasty stuff will AGI come up with.
If you don't already know category theory, learning it is hard. The terms on wikipedia seem to form a dense graph of links. It's hard to get a foothold of comprehension. For people that already know C++, or are at least familiar with this syntax, this is more useful than describing it in haskell syntax or category theory. There seems to be a chicken and egg problem regarding haskell and monads. Learning c++ may be harder or easier than category theory. I'm no sure, as I don't understand either one of them. But this syntax makes more sense to me than something expressed in terms of category theory vocabulary.
Learning category theory to the level of understanding monads should take half an hour at most, and would constitute real understanding of what a monad is, versus this C++ explanation which is handwavy even in terms of C++. C++ can't even encode monads accurately!
But one doesn't even need to learn category theory. I assume that everybody has learned abstract algebra in high school, monoid, rings, groups, vector spaces and all that. A monad is just another kind of a structure like that. If you have studied abstract algebra in school then it should take 5 seconds to read the definition of a monad, a minute to understand it, and perhaps 10 minutes to see how various things such as errors or lists form monads.
Learning category theory, or indeed any sort of math from Wikipedia is an absolute futile endeavour.
I learned none of those in high school or university. I did indeed fail for much more than 30 minutes to learn any of them from Wikipedia and other sources.
Over the years I've spent many hours trying to make any sense of monads with varying degrees of success. But mostly not.
Your assertions do not seem consistent with reality as I've observed it.
At least in my country (the UK), people generally do not learn abstract algebra in high school. That's a university-level topic.
I think there is a definite "step up" in complexity between the structures of abstract algebra such as monoids, rings, groups and vector spaces, and monads. All of those algebraic structures are basically just sets equipped with operations satisfying some equations. Monads are endofunctors equipped with natural transformations satisfying some equations. "Endofunctor" and "natural transformation" are considerably more advanced and abstract concepts than "set" and "operation", and they are concepts that belong to category theory (so I don't see how you can read and understand the definition of a monad without that basic level of category theory).
Your time estimates also seem wildly optimistic. A common rule of thumb is that reading a maths textbook at your level takes around an hour per page. I think the definition of a monad can be compared to one page of a textbook. So I'd say it'll take on the order of hours to read and understand the definition of a monad, and that's assuming you're already entirely comfortable with the pre-requisite concepts (natural transformations, etc.)
> To avoid Russell's Paradox, there isn't a type of all types. Instead, we have universes.
This is an oversimplification, and Lean-specific (to be fair, the author claims to explore these concept in Lean). Girard's paradox comes from unrestricted impredicativity. To maintain consistency one needs to control impredicativity, type universes are a possible, very straightforward choice, but it is not the only choice.
Some theorem provers, such as Cedille, do not use type universes, and even have `Type : Type` while still being consistent. See Stump, Aaron: “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27 (2017): e14. DOI:10.1017/S0956796817000053[0]
Additionally:
> The famous Curry-Howard correspondence states [...] Propositions are types in Prop [...]
Curry-Howard doesn't say anything about Prop, Prop vs. Type is just a distinction done in some particular type theories for pragmatic reasons, or because it simplifies classical (as opposed to intuitionistic) reasoning. In fact the reason why Prop vs. Type is a distinction done by many theorem provers leads Lawrence Paulson[1] to claim that modern theorem provers don't really use Curry-Howard[2], at least as Curry-Howard was originally defined. I disagree, because elements of Prop are still types, but please understand that this is a departure from original Curry-Howard.
Moreover:
> The famous Curry-Howard correspondence states [...] True propositions have exactly one term [...]
As explained above, this is not the case for the "original" Curry-Howard, and it is just a choice in Lean, which is a type theory with proof irrelevance. There are different type theories without proof irrelevance (such as Adga by default without a recent extension), and Curry-Howard certainly still applies to them. In fact even in Rocq (Coq), which still has Prop vs. Set, proof irrelevance has to be assumed explicitly[3]. (Rocq also has SProp[4] for proof irrelevant propositions.
nLab has more information about propositions as types[5] vs. propositions as some types[6].
HDR is about, well, high dynamic range images, usually expressed with at least 10 bits of precision (although it can also be float, etc), and often, but not always encoding scene-referred data instead of image-referred data (originally it was supposed to only encode scene-referred data, but then other competing formats ignored that). It has nothing to do with the gamut and with the color primaries, although in practice HDR images use a large color space.
But you can absolutely have an SDR image encoded using a large color space. So I am not sure why the author talks about color primaries when it tries to justify HDR… I still don’t know what kind of HDR images this new PNG variant can encode.
> This post is mostly AI generated, of course with significant guidance, feedback, iteration and some edits from me.
I can tell, because it is garbage.
AI's notion of PK is useless because of Blum's speedup theorem. Because the invariance theorem fails in PR (PR is not universal), description-length gaps between PR and Turing complete languages can grow without bound.
Essentially a more expressive formalism can encode an interpreter for the weaker one and then diagonalise over it. Restricting yourself to a total language, you sacrifice potentially unbounded conciseness.
This is a profound difference between TC and non-TC languages, and it manifests even for terminating functions. It's not just that a TC languages can encode non-terminating computations, it's that a TC language can encode terminating functions more efficiently than a non-TC language. A terminating program expressed in a total language must manifest its termination proof in a strict way with finite degrees of freedom, whatever the choice of total language might be. In a TC language it doesn't have this artificial constraint.
In some sense, as program complexity grows (expressed in a total language), more and more of the program is dedicated just to encoding its own termination proof. We can sort of see this a corollary of this experimentally with programs (proofs) written in theorem provers like Coq (which are total). Giant proofs extract to very small programs. We don't see the sort of phenomenon in theorem provers using a Curry-style type system, for example Nuprl, where the underlying lambda calculus is Turing complete. This is experimental evidence that even though most interesting functions might be PR, a PR language might not be the best language to express those functions. And this seems to be the case even without choosing specially-crafted pathological examples.
These are subtle issues and I can't fault the author for not knowing about them, but I can fault him for using AI to appear to say something profound when all that was said was woefully naïve.
Since the author seems to be concerned about tractable inductive inference, and to be honest computability does not give you much, what do you think about the utility of notions like resource-bounded Kolmogorov complexity for that?
I want the opposite, an extension that will redirect all crappy frontends to the canonical sources (which work better and I am logged-into, I can comment, etc).
Indeed, KDE is like Windows, which is sad, because I don't like the desktop metaphor, yet KDE is the only group that is concerned with usability and improves the system with every release.
I actually don't mind the GNOME metaphor... but they make it less and less usable over each release. Philosophically, what they are talking about sounds great, but pragmatically the system is just getting less and less usable. UX consistency is good, but not when it comes at the expense of functionality. Also, I don't like that GNOME has been ideologically captured by the extreme left.
Back in the day I ran WindowMaker and FVWM, but nowadays, with Wayland, HiDPI screens and expectations of integration, it is not a viable strategy anymore.
Usable and lack of additional functionality are absolutely different things. Gnome is the most usable DE in linux, and a default for major distributions for a reason. It’s simple, it’s coherent, pretty much never breaks and just in general designed to bother you as less as possible so you can just do your work.
KDE tries to satisfy anyone with all kinds of options, but as a result most of such options are half baked and DE starts to fall apart with memory leaks and inconsistency as soon as you’re deviating from default experience enough. I do like KDE’s innovations and attempts to get as maximum performance as possible, but sad truth is that in he last 15 years I’m trying fresh KDE once in a year or two, but have to crawl back to gnome after about a week, as small but annoying problems, memory leaks or inconsistencies result in frustration.
> general designed to bother you as less as possible so you can just do your work
I have heard this so many times about Gnome yet no one explains how a desktop environment can "bother" a user so that they can't focus on their work. In fact, Gnome decision to show notification at the top middle of screen is the most distracting thing a DE can do.
I agree that plasmashell does have memory related issue but at least it is not part of the compositor (unlike gnome-shell which is the desktop shell and the compositor using mutter library) so that you can just kill it and restart it without having to logout.
Comparison with TLA+ doesn't make any sense as TLA+ implements a very different sort of logic, but the property that it is a real programming language is shared by virtually everything in this space.
Lean/Adga are real programming languages, while Coq (Rocq), F*, ATS, Isabelle/HOL all extract to various other programming languages.
Agreed, my remark was more coming from the point of view that I don't get why TLA+ keeps being talked about, when there is such an impedance mismatch between the math model proving the logic, and the actual implementation, where even the language semantics might play a role that wasn't clearly mapped on TLA+ model.
Isn't TLA+ is more like Alloy insofar as they're thinking tools optimized for the design phase?
I'm more familiar with Alloy, which is a great tool for exploring a specification and looking for counter-examples that violate your specification.
AFAIK, none of the languages you listed above work well in conceptualization phase. Are any of them capable of synthesizing counter-examples out of the box? (Aside: I feel like Lean's meta capabilities could be leveraged to do this.)
I only listed Dafny, although I do agree with the list on the reply to me.
Never looked into Alloy, I guess have to get an understanding of it.
How can you validate that the beautiful design phase actually maps to e.g. C code, writing data via ODBC to a SQL database, with stored procedures written in PL/SQL?
Neither the semantics of the toolchains nor the semantics of the commercial products ar part of the TLA+ model as such.
Additionally it requires someone to meticulously compare the mathematical model with the implementation code, to validate that what is written actually maps to what was designed.
Although it wouldn't work for my contrieved example, at least tools like Dafny have more viability by going through "formal model => generate library for consumption", so that we can get an automated model to code validation, without human intervention.
> Additionally it requires someone to meticulously compare the mathematical model with the implementation code, to validate that what is written actually maps to what was designed.
This is a deficiency in TLA+ (and many other systems), but it's not a good enough reason to discard or dismiss it. The industry alternative to TLA+ is not something that traces fully and easily from spec to code, but mostly to use informal, largely prose, documents as their specification (if they specify anything at all). TLA+ is a massive improvement on that even if it's not a perfect tool. Same for Alloy and other systems. It's better if people model and specify at least portions of their system formally even if it still takes effort to verify the code correctly implements that specification, effort they have to expend anyways but with greater difficulty lacking any thing approaching a formal specification.
Dafny is great, and has some advantages compared to its competitors, but unequivocally calling it "the best" is quite bullish. For example, languages using dependent types (F*, ATS, Coq/Adga/Lean) are more expressive. And there are very mature systems using HOL.
Truth is that everything involves a tradeoff, and some systems are better than others at different things. Dafny explores a particular design space. Hoare-style invariants are easier to use than dependent types (as long as your SMT solver is happy, anyway) but F* also has that, except that in F* you can also use dependent types when automatic refinement proofs become inadequate. And F* and ATS can target low-level, more so than Dafny.
Probably I would not use ATS for anything, but between F* and Dafny, there isn't such a clear cut (I'd most likely use F*).
And if I don't need (relatively) low-level, I wouldn't use either.
I think poor countries with weak democracies or dysfunctional systems would do pretty good with AGI. I don't believe democracy will survive AGI, except, perhaps in the United States.