I can’t really relate to this article at all but I couldn’t help but think if Emmanuel wants to work so hard why doesn’t he just take up what I did very recently in lifting heavy things in a warehouse all day? He has already taken the meritocratic mythos at its face so it’s almost comedic how few questions he asks about how the most severely overworked people in the market are structurally the most underpaid. If I shared the privileged sob story “I get paid so much and work so little” with any of my old blue collar colleagues it’d just piss them off and not for the reason he thinks it would.
Do you mean you didn’t get the vibe from the article or that you didn’t get why they used that emotion for the article?
He repeatedly mentions how “boring” it is and how it feels so “ethically compromising” to not meet his own abstract notion of merit… I guess if you’ve never had to struggle for money in your life maybe that would sound like an actual, serious problem to have. Personally as long as I’m not building machinery for the military death cult or some other similarly bleak occupation I really couldn’t give a damn about how little effort it takes to feed my family but I’ll just pin that on having vastly different priorities.
I see: you read a personal story about someone being sad they’re not living up to their full potential. I read an analysis about a systemic problem that is wasting everybody’s time (and resources if there’s a commute) and stifling whatever collective progress we could make.
Also consider that fixing the most inefficient sectors could have nice collective benefits, such as reducing the work week at little to no economic cost, or reallocating resources that are currently wasted to those who are struggling for money.
Edit: also, I object to your suggestion that someone should not complain because others have it so much worse. By that logic no Lobster fortunate enough to even be able to read this comment shouldn’t complain, because somewhere around the world there is someone who has it so, so much worse. I’ll refrain from giving any example, to avoid triggers.
I guess if you’ve never had to struggle for money in your life maybe that would sound like an actual, serious problem to have.
It is entirely possible that the author has had that struggle; I did not see evidence in the article either way. I don’t think it helps the discussion to dismiss an author based on things we assume about them.
I really couldn’t give a damn about how little effort it takes to feed my family but I’ll just pin that on having vastly different priorities.
Exactly–your prioritization of your family is just as valid, to you, as (I presume here) the author’s prioritization of living up to their capabilities is to them. If you expect that we should not care about their unhappiness, we certainly cannot be expected to care about your family’s. You and the author are different, and value judgements as to who is suffering more or prioritizing better aren’t–I believe–really good material for conversation.
But isn’t saying that one view is valid or not a moralistic judgement and is therefore not sufficient for “economic decision-making” 🤔
the most severely overworked people in the market are structurally the most underpaid.
The supply of people who can lift boxes in a warehouse dwarfs the supply of people that can bang on keyboards productively, at least for now. These are different markets.
That explains why (society|employers) get away with underpaying them. It does not change the fact that the people who lift boxes in warehouses are underpaid.
If they keep showing up to work they’re getting paid exactly what they’ve valued their labor at.
Does desperation cause people to value labor their labor lower than they otherwise would? Sure. Do companies and society at large benefit from and promote policies that encourage patterns of consumption and thought that make it more likely to be desperate for work? Absolutely.
That said, I think the notions of “underpaying” and “overpaying” are not by themselves useful and lend to a moralistic worldview that is insufficient for economic decision-making.
A predilection for “economic decision-making” over concern for the wellbeing of human life is itself a moralistic worldview. A pretty disturbing one in my opinion
I find it particularly inhumane to expect people to acquire and maintain any degree of wellbeing while also telling them to ignore basic facts about how the systems they interact with function merely because those systems are immoral and evil and inhumane.
People are not going to be able to live their best lives if they cannot reason about the world, and there are more perspectives required for reasoning than solely “is this humane?” or “is this evil?”.
Anyways, we’re getting well off into the weeds for this site–hit me up in DMs if you’d like to talk more on the topic. I’m not, by my own estimation anyways, an amoral monster.
You don’t need to ignore or misunderstand things to think they’re evil. Hierarchies like Capitalism are not that complicated. You take a power imbalance (some people controlling more stuff than others, and thus having the luxury of patience) between a few groups, a leverage mechanism (paying people a small amount of stuff to use your stuff to make you much more stuff), and reinforce it with some fixed ideas (The State / The Law / God / Meritocratic Myth) and boom, you’ve got yourself a self-sustaining exploitation machine.
People cannot live their best lives if they uncritically believe the narratives created by the people who control them, and would like to continue doing so, either.
Another point of view is that optimising economic decision-making over morality has benefited the wellbeing of people on average than optimising purely for morals.
Do companies and society at large benefit from
Companies benefit. Most of the key decision-makers benefit, as do most of the wealthiest ~20-30%.
Society at large is made of the people who end up desperate enough to wreck their bodies for a pittance.
The “capitalism is evil” folk are responding to the practical outcome of those with capital having more influence over government policy than those without, resulting in policies that tilt the scales in their favor.
Your viewpoint is either fine or reprehensible depending on whether you believe that those who do not work should not eat. If those who do not work should eat nonetheless, then it is fine to undervalue labor; labor is optional. But if there is no food for those who do not work, then labor must be valued enough to be fungible for sufficient food and shelter on the open markets; in other words, a minimum living wage is necessary.
It’s not our fault that you’re constantly obscuring your actual beliefs and thus making it harder to evaluate your position.
There are two ways to understand these kinds of problems in my view.
There is firstly the apparatus-oriented view you espouse. This kind of view builds an apparatus out of abstract norms (i.e. demand) to which it then molds its observation of reality into, discarding whatever the apparatus doesn’t account for until the apparatus fails its own, internal measure of empirical success. At which point that apparatus is either adjusted to fit the previous internal measure of success or a new apparatus is conceived to “fit the data” so to speak.
This kind of view comes with a variety of problems that present themselves as a kind of blindfold. Although resembling a scientific process with hypotheses, observations, and a notion of fallibility, these apparatuses are exceptionally susceptible to personal biases in their construction, allowing for a kind of categorical failure where the limited internal notion of fallibility are blinded to data which doesn’t conform to the preconceived internal measurements. Additionally the criteria of “success” for these models of reality are themselves preconceived from individual biases, and therefore fail to look further than the author of the apparatus cares to see.
The second kind of view I prefer however is an unprejudiced historically-centered one. This kind of view begins with observation instead of ending with observation. This kind of view can look past simplifications such as “less keyboard people than lifting-capable people” and see, for example:
Not one of these aspects of historical reality can be accounted for with the view of an economic apparatus, because that apparatus was constructed to comprehend the dynamics of exchange while flattening the circumstances of exchange. That is all to say, I don’t agree they are just “different markets”. And I can tell you this from, at the very least, the reality of the incredibly skilled and intelligent people I’ve met, who for myriad reasons, are forced to destroy their bodies to feed and house themselves and their loved ones.
There are all kinds of other interesting historical facts and pathos-friendly factors one can drag up.
There’s also the obvious point that the labor market for warehouse labor requires a) a strong back and b) the ability to follow basic instructions, and the labor market for tech stuff requires a) the ability to communicate effectively, b) the ability to type, c) the ability to program, d) the ability to discover solutions to novel(ish) problems. These are different jobs, and ones that require different labor groups (though most programmers could probably do the warehouse job if they needed to).
(And yes, there are exceptions to both markets, but I think they’re rare enough as to not matter in making my point.)
I really don’t think this should be particularly controversial–different forms of labor require different levels of skill, different levels of skill correspond to rarity of workforce, and rarity of workforce increases bargaining power and thus wages.
(And yes, there are cases where this model is insufficient. That is not the majority of cases.)
If you believe my point is that “certain occupations don’t require certain skills” you’ve really severely misread what I’m trying to say. Obviously certain occupations require certain things of people, I’m not stupid. My point is that you seem to rhetorically take this requirement to be the single normative condition upon which people are forced or not to perform certain labor, and in the process neglect all other circumstances, big and small, which shape the evolving realities of labor.
supply of people that can bang on keyboards productively
The article is not about people who can bang on keyboards productively; it’s about people who can produce the illusion of productivity. There’s lots of money to be made in potemkin villages, and it doesn’t require skilled labor.
I know it’s not central to the point of the article, but I don’t think Pulumi will be relevant in ten years except at businesses that start to use Pulumi in the next ten years. The upside to Pulumi of it using a language you already know the syntax of is cool and quirky but I don’t care if technically it’s declarative because you build a DAG, it’s still written in imperative, turing-complete code with all the footguns that brings.
So far every time I’ve had to deal with infrastructure, I’ve ended up using “imperative, turing-complete code” to “build a DAG”, because traditional tools just aren’t good enough. And I think that’s mostly because there is very little abstraction capabilities using tools that are essentially configuration languages with some primitive templating support. Just look at what has to be done in Terraform to have optional components - you have to set the count of them to imitate a simple
The main benefit of such tools isn’t that they bring you the syntax of conventional languages, but that they bring you abstraction capabilities of conventional languages - and I feel like that’s not being properly advertised by any of the existing tools. But I can say that the abstraction capability has helped people in my team that aren’t “infrastructure specialists” to regularly contribute to infrastructure, and not because they don’t need to learn Terraform, but because they can freely compose abstractions that people with more experience in infrastructure have already built.
if” is only simple because you’re doing something simple and I assume you’re a pretty smart, switched-on guy with good coding hygiene. The logic behind count is perfectly fine - it’s not “imitating” an if-statement, it’s a loop with a counter, which will happily be set to 0.
Enabling or disabling components by setting their count leaves the same taste in my mouth as only using lambdas to program in Python does - you can do it, but it’s definitely not the best way of doing it and you are loosing a lot of clarity by doing it this way.
A genuinely baffling vulnerability. Absolutely astounding that an image crop can’t just be an image crop. If only there were an avenue for this to get Google in legal trouble.
This is unfair. The image crop does everything you would expect assuming you were doing it yourself. The bug is an undocumented change to the IO routine. Specifically prior to android 10 there was a file IO routine, that takes a mode flag like C’s open, where you open a file to write by passing
"w", e.g. open(“a.png”, “w”)`. That opens the file for writing, and if the file already exists the output is truncated to 0 size.
So the code for editing the image did (pseudo code):
pathToImage = "path/to/image" someImageFile = fopen(pathToImage, "r") someImageObject = parseImage(someImageFile) fclose(someImageFile) editImage(someImageObject) // crop stuff, user editing UI or whatever. This is just pseudo code // Now save in place outputFile = fopen(pathToImage, "w") someImageObject.storeImage(outputFile)
This is essentially what google was doing, but instead of fopen() they were using an android API that took the mode string. The important thing is that when you open a file for writing with “w”, if the file already exists then it is truncated to zero bytes, e.g. it’s functionally a new file.
That is the way the android API worked, which makes sense: you’ve got an API modeled after another API you should be consistent with that other API. At the point this image editing code was written everything was fine: crop, culling, redacting, etc your image is fine.
But then in android 10 someone made a change (and apparently didn’t document it) that broke bincompat by changing the behavior so the default behavior. Now opening a file to write with “w” stopped erasing the old file, so the above code - with no changes - started leaking private user data. So where previously you got
o for original
n for new)
but post this bincompat breaking change you get
Now depending on what and where the image was edited you can reconstruct the state of the compression in the original image, so you can recover the original pixels from the tail of the “edited” image.
It’s important to note that any program editing a file of any kind would start leaking information like this if the the underlying IO functions were changed like this (imagine how bad the result of changing this behavior in
fopen() would be).
The long story short is: the image editing was done correctly, and wasn’t doing anything “stupid”. An underlying library decided that their API wasn’t good and decided to change it, but they changed it after it was already in use, which is just not something you can do without creating this kind of problem. That’s why API design takes time, and why “API stability” doesn’t just mean ABI stability.
My comment was posted prior to the technical write-up about the discovery of the bug, or explanation of the underlying API change, was made public (afaik). It’s still baffling, even knowing the reason (baffled by such a change to the API being used, going undocumented and subsequently unnoticed).
models still have many deficiencies: they can generate false information, propagate social stereotypes, and produce toxic language
Honestly I don’t really understand what’s the issue with an AI generating !woke language. What if I want it to help me write the dialogs of a 17th century slave owner? Why are they imposing such limitations, it seems silly. Who will it hurt?
Minority groups, probably. The issue is not that the model is capable of generating such text, but that humans are using the text. If humans didn’t enjoy spreading false information and ignorant stereotypes, there would be little need to mitigate the generation of that information.
There’s clearly a distinguishing factor between “17th century slave owner” dialogue and the more general “toxic language”. It’s odd that you see the opposite of “toxic” as “woke”, as opposed to something more like “polite”.
models like these can be used to strengthen nationalist/fascist movements through spam, and manufacture consent for harmful policy
c.f. Hindu nationalist movements in india
I love the name.
Also, I’ve wanted something like this several times in the past few years, particularly for stuff that starts out very ad hoc that I then want to share with someone.
pip freeze is a little rough for that, and FawltyDeps seems at first blush like it’d smooth that out quite a bit.
Thanks for building and sharing this.
We emphasize that Alpaca is intended only for academic research and any commercial use is prohibited
So it’s not an open-source model, why would that be in the title of their paper?
This is also a feature by default in Fish shell - when you go to enter arguments, it’ll print the arguments to a command and their description from the manual or help page in a navigable list format.
From the gifs on the page
halp tries different combinations of
--help, etc… until help text (any text?) is printed, or it’s exhausted the usual options.
I’m really glad this book is being written and hopefully it helps Nix getting more traction and better documentation! I associate the word production with professional deployments and I think the cover with the anime character and furry-like attributes is sending the wrong signal.
I think it’s supposed to be reminiscient of textbooks such as “The Manga Guide to Physics”, though the content of that was a manga that taught you physics.
Perhaps what we currently deem professional is about to undergo a world of change and stark deviattions such as this is a harbinger of such change.
I would hope not. Bland and boring is least alienating, both to different demographics and different time periods.
Edit: Changed my mind - burn it all down
I don’t think “low power” and sustainability are synonymous - but the tag system is primarily for filtering out content, not finding it. These articles usually have keywords: degrowth, “battery life”, “low tech” etc., and so it really seems more like a tag for it’s own sake rather than a tag for the necessity of excluding content from your feed. I guess tag bloat is a silly thing to worry about but overtagging and hyper-specialisation of tagging doesn’t really seem to bring so many benefits vs. using the search system.
It’s also a way to indicate that such content is welcome - the story submission guidelines say that if there’s no suitable tag, you should reconsider your submission. Now they’re typically tagged with a tangentially related tag.
Docker builds are not deterministic. If you build an image twice with the same exact same contents, it may produce a different hash each time. (While not directly relevant, we wanted to note this unexpected observation. As a corner case, consider that a freshly built large layer that is identical to a layer already in the registry may still get uploaded as a new layer.)
Nix actually fixes this with
Is the EU bureaucracy going to pay the increased costs of developing these utilities and requirements in code, or is that being left to industry as to further suppress salaries and raise prices?
idk, is industry going to pay the costs associated with their users and customers having their PII stolen and downtime due to their systems failing, or will those costs just get transparently passed on to the customer or soaked out of their own workers’ wages to keep stock prices high?
There’s seldom one side to any story.
Software notoriously has ridiculous profit margins. That’s why you hear so many companies trying to grow the “services” section of their income pie chart. There is plenty of room for some minimal cybersecurity requirements to be imposed (not saying the ones in this article are the right balance).
Also consider the staggering cost of insecure software. It’s rich for well-paid software workers to complain of suppressed salaries when everyone else is paying billions to trillions every year for our own carelessness: https://www.cisa.gov/sites/default/files/publications/CISA-OCE_Cost_of_Cyber_Incidents_Study-FINAL_508.pdf
If it is, it will be through increased taxation, and “everyone” pays.
Raised prices makes Chinese import even more affordable and no one will care about any regulation in that context.
Sweet ideas on paper, but this will likely hurt most where it should do the most good.
Wonder how this differs from https://github.com/jetpack-io/devbox
One difference is that devbox wants to almost completely hide nix from you. For example, it automatically installs it for you. The abstraction is thicker, for sure.
My very naive guess at which you should play with, based on how I decided: if you want an abstraction over nix that you can adopt without ever hearing the word nix, give devbox a try. If you want something to ease you into using nix before you dive in head first, give devenv a try. I have very low confidence that’s a good or accurate heuristic.
Hi all, I’m the founder of jetpack.io (developers of Devbox), and I agree with your take:
Devbox is trying to give you the power of nix, but with a simplified interface that matches the simplicity of a package manager like yarn. If you want reproducible environments by simply specifying the list of packages you depend on, and not having to learn a new language, then devbox is a great match.
On the other hand, if you’re trying to do something that is involved and requires the full nix language, then devenv can be a great match.
and it uses json as a surface language, with all the limitations this implies compared to nix-lang.
yea, that’s what i surmised just from a cursory look… the devbox abstraction might be quite limiting in some ways, whereas devenv seems thinner and probably therefore less leaky (because it’s designed to leak?)
I feel like this is misleading (I’m the founder of jetpack.io the company that makes Devbox)
Yes, jetpack.io is a for-profit business: but we’ve committed to making the Devbox OSS tool free forever. We plan to monetize by offering managed services (Devbox Cloud), but those are an independent codebase, and you only need to pay for them if you want the managed services. If you don’t, then Devbox OSS is, and will forever be, free and completely open source.
This is similar to how Cachix is a for-profit business. It offers a Cachix managed service that it monetizes. It is commited to making devenv a free open-source project. You only need to pay for cachix if you want to use the managed service.
In that sense, both companies/projects monetize in a similar way.
Abstracted support for services, language versions, etc. It’s basically an alternative that’s both simpler and provides more features up front. But may not support the advanced tinkering. If you need to do more than devenv can provide, you can always revert you shell.nix
Way easier to understand if just some random guy on your team wants to add a package or shellHook or whatever.
My shower thought on Nix the other day was “they’re trying to boil three different oceans, and I really only want them to boil one.”
Packaging binaries. The other oceans are cool too, but I’m sort of in Julia’s camp of just wanting to install some stuff.
The Nix programming language is a purely-functional programming language, not a configuration language. It’s used to program the Nix package manager in the same way as any other programming language would. It just happens to be good at configuration :^)
You can get Nixpkgs to run on any other Linux distro (and on Mac too), so you don’t need to boil that third ocean if you don’t want to.
I have become one of those boring people whose first thought is “why not just use Nix” as a response to half of the technical blog posts I see. The existence of all those other projects, package managers, runtime managers, container tooling, tools for sharable reproducible development environment, much of Docker, and much more, when taken together all point to the need for Nix (and the need for Nix to reach a critical point of ease of adoption).
The Nix community has been aware of the DX pitfalls that prevented developers to be happy with the tooling.
I’ve made https://devenv.sh to address these and make it easy for newcomers, let me know if you hit any issues.
+1 for devenv. It’s boss. The only thing I think it’s truly “missing” at the moment is package versioning (correct me if I’m wrong).
it doesn’t appear to support using different versions of runtimes—which is the entire point of asdf/rtx in the first place. I’m not sure why I would use devenv over homebrew if I didn’t care about versions.
I think the idea is a
devenv per-project, not globally, like a
.tool-versions file; as you say, it’d be a bit of a non-sequitor otherwise
Primarily the bad taste the lacking UX and documentation leaves in people’s mouths. Python development is especially crap with Nix, even if you’re using dream2nix or mach-nix or poetry2nix or whatever2nix. Technically, Nix is awesome and this is the kind of thing the Nix package manager excels at.
mach-nix very usable! I’m not primarily working with Python though.
because the documentation is horrible, the UX is bad, and it doesn’t like it when you try to do something outside of it’s bounds. It also solves different problems from containers (well, there’s some overlap, but a networking model is not part of Nix).
I’ll adopt Nix the moment that the cure hurts less than the disease. If someone gave Nix the same UX as Rtx or Asdf, people would flock to it. Instead it has the UX of a tire fire (but with more copy-paste from people’s blogs) and a street team that mostly alienates 3/4 of the nerds who encounter it.
Curious did you try https://denvenv.sh yet?
https://devenv.sh for those clicking…
No, thanks for the link! This looks like a real usability improvement. I don’t know if I am in the target audience, but I could see this being very useful for reproducing env in QA.
It’s like using kubernetes. Apparently it’s great if you can figure out how to use it.
I’ve given up twice trying to use nix personally. I think it’s just for people smarter than me.
Heh, that’s a good counterpoint. I would say, unlike with k8s I get very immediate benefits from even superficial nix use. (I do use k8s too, but only because I work with people who know it very well.) I assure you (honest) I’m not very smart. I just focus on using nix in the simplest way possible that gives me daily value, and add a little something every few months or so. I still have a long way to go!
How it works section of the
rtx README sounds very much like nix + direnv! (And of course, I’m not saying there’s no place for tools like
rtx, looks like a great project!)
Nix is another solution that treats the symptoms but not the disease. I used asdf (and now rtx) mainly for Python because somehow Python devs find it acceptable to break backwards compatibility between minor versions. Therefore, some libraries define min and max supported interpreter version.
Still, I’d rather use rtx than nix. Better documentation and UX than anything Nix community created since 2003.
Sure. It’s good that a better alternative for asdf exists, although it would be better that such a program wasn’t needed at all.
Isn’t it somewhat difficult to pin collections of different versions of software for different directories with Nix?
Yes it is difficult. Nix is great at “give me Rust” but not as great at “give me Rust 1.64.0”. That said for Rust itself there aren’t third party repos that provide such capability.
I think you are pointing out that
nixpkgs tends to only ship a single version of the Rust compiler. While
nixpkgs is a big component of the Nix ecosystem, Nix itself has no limitations prevent using it to install multiple version of Rust.
Obviously nix itself has no limitation as I mentioned there are other projects to enable this capability. While you are correct I was referring to nixpkgs, for all intents nixpkgs is part of the nix ecosystem. Without nixpkgs, very few people would be using or talking about nix.
I thought that was the point of Nix, that different packages could use their own versions of dependencies. Was I misunderstanding?
What Adam means here is that depending on what revision of Nixpkgs you pull in, you will only be able to choose one version of rustc. (We only package one version of rustc, the latest stable, at any given time.)
Of course, that doesn’t stop you from mixing and matching packages from different Nixpkgs versions, they’re just… not the easiest thing to find if you want to be given a specific package version.
(Though for Rust specifically, as Adam mentioned, there are two projects that are able to do this easier: rust-overlay and Fenix.)
This is a great tool to find a revision of Nixpkgs that has a specific version of some package that you need: https://lazamar.co.uk/nix-versions/
That said, it’s too hard, and flakes provides much nicer DX.
for Rust specifically, […] there are two projects that are able to do this easier: rust-overlay and Fenix
The original https://github.com/mozilla/nixpkgs-mozilla still works too, as far as I know. I use it, including to have multiple versions of Rust.
No I wouldn’t say so, especially using flakes. (It gets trickier if you want to use nix to pin all the libs used by a project. It’s not complicated in theory, but there are different and often multiple solutions per language.)
nix-shell -p nodejs-18_x jq nodejs -v jq --version
Docs https://nixos.org/guides/declarative-and-reproducible-developer-environments.html or use https://devenv.sh/
These are some quick ways to get started:
Without flakes: https://nix.dev/tutorials/ad-hoc-developer-environments#ad-hoc-envs
With flakes: https://zero-to-nix.com/start/nix-develop
And add direnv to get automatic activation of environment-per-directory: https://determinate.systems/posts/nix-direnv
Or try devenv: https://devenv.sh/
(Pros: much easier to get started. Cons: very new, doesn’t yet allow you to pick all old versions of a language, for example.)
Supposing that a language model ever becomes smart enough to be genuinely terrifying, one imagines it must surely also become smart enough to prove deep theorems that we can’t. Maybe it proves P≠NP and the Riemann Hypothesis as easily as ChatGPT generates poems about Bubblesort. Or it outputs the true quantum theory of gravity, explains what preceded the Big Bang and how to build closed timelike curves. Or illuminates the mysteries of consciousness and quantum measurement and why there’s anything at all. Be honest, wouldn’t you like to find out?
This is the type of thing that GPT cannot do. For an AI to do these tasks it would need to be much more than just a language model.
I see GPT as an incredibly powerful search engine that is it capable of composing a response rather than just giving you a list of links.
When it comes to AI safety, my belief is not so much that an AI will go foom, break out the box, or create a grey goo nanomachine scenario. My worry is that it will influence large numbers of people to cause harm. This is a much lower hanging ‘fruit’ in terms of AI disasters because the requirements on the intelligence of the AI are much lower.
The premise of the Terminator franchise is a lot more plausible without the SkyNet-became-self-aware step. An LLM entering a bit of its prediction space where launching all of the nuclear weapons because the input data happened to correlate with something unexpected seems entirely plausible.
AI safety to me is “what do we do when an AI-led competitor to Qanon eventually shows up?” and nobody seems to have an answer for this. “Turn it off”, lol.
I disagree: I think this is the type of thing that GPT can do. The vast difference in difficulty simply makes it seem like a higher class of task, but I think that’s mistaken. Theorem proving in particular “just” consists of repeated application of formal rules. The difference is in choosing which rules to apply, which seems to require both strategy and a particular sense of elegance. I see no reason that a language model could not acquire this sense.
I don’t think this is an accurate representation of what proving is like. While you can limit it to “just” repeated application of formal rules, even the simplest possible systems which can’t prove almost anything, like Presburger Arithmetic, are 2-EXPTIME. PA is just quantified boolean logic plus addition (but not multiplication) of natural numbers. You can automate the proof or disproof of any statement of length N representable in PA… but the worst such statements will (provably!) take O(2^(2^N)) steps. And that’s an incredibly simple system!
Mathematicians primarily work by stepping outside the “formal rules”: finding new grammar or language to express complex ideas more compactly, but also consistently. In other words, there’s an infinite number of possible rules, and it’s a matter of finding the right rules and showing they’re right. That’s an intensely creative and messy process.
For a lot of proofs, the key thing that a human is doing is providing a hint about the path through the search space. For a long time, theorem provers couldn’t go past an EFQ step because there are an infinite number of possible steps immediately after it and only a handful lead to a proof. Then they gained heuristics that let them make this jump in a few cases.
Anything where the current state of the art is ‘we have some heuristics but they’re not great’ is likely to see big wins from ML.
Theorem proving in particular “just” consists of repeated application of formal rules.
Right in a computability sense, but it is a bit more complex complexity-wise. This is like saying “all NP-complete problems are just computable”. To prove things in a reasonable time, you need to be able to define things (concept formation). It is known that avoiding a definition can increase the proof length super-exponentially.
To solve difficult problems you need to “think” before you speak.
GPTs ability to think can be augmented by asking it to explain its steps. This is a clever hack that makes use of the way a language model uses prior context to complete further lines. My belief is that this is not going to scale up to solve difficult computational problems that involve modelling, planning and calculational brute force via tree search. We would need to integrate things like alphazero. but also other things that haven’t been invented yet.
A multimodal model should be able to “think” in more modes. Imagine a ChatGPT version that can interrupt its Chain of Thought to insert a sketch generated from its previous prompt, then condition on that sketch when continuing.
(I was worried about posting this, then I remembered that if I thought of this within five minutes, OpenAI/Deepmind have definitely thought of it.)
Sure, but such capability has not been demonstrated yet, at least not convincingly.
FeepingCreature (and many others) seems to view proof search as similar to game tree search, such that AlphaZero-like methods can work. In fact, AlphaZero-like methods do work, for short proofs. But proofs, when definitions are substituted, can be arbitrarily long, and long proofs in practice are very unlike searching for sequence of moves. It is more like searching for a program, when executed, generates sequence of moves (and short program can generate very long sequence).
This is best answered with reference to the transformer architecture
The input is tokenized and the tokens are put through an ‘encoder’ block which has a self-attention and a feed forward neural network before being given to the decoder path.
This encoder network is very large which enables the system to produce such high quality output. But there is fundamentally no way for this to perform tree search. It isn’t a capability that it can learn.
I don’t think tree search is absolutely necessary. Remember that AlphaGo Zero could beat most amateurs without any tree search (simply playing a move with the highest win probability).
Rather, I consider characterization of proof as “repeated application of formal rules” to be incorrect. Yes, proof is that, but interesting proofs written that way are 2^2^n tokens or more long. In practice, proofs can’t be generated in expanded form and need to be generated compressed, and compression is where the difficulty is, not the choice of which rules of inference to apply.
It’s true. People are already writing content to draw other people into their own epistemically closed communities (somewhat like a cult), and those communities seem to be closely affiliated with mass shootings in the US and related phenomena like Islamic State.
ChatGPT vastly improves the productivity of producing such propaganda content if you don’t care about its accuracy or verifiability.
not so much that an AI will … create a grey goo nanomachine scenario
Kurzweil also supports the idea of grey goo being a non-issue.
The smallest plausible biovorous nanoreplicator has a molecular weight of ~1 gigadalton and a minimum replication time of perhaps ~100 seconds, in theory permitting global ecophagy to be completed in as few as ~104 seconds. However, such rapid replication creates an immediately detectable thermal signature enabling effective defensive policing instrumentalities to be promptly deployed before significant damage to the ecology can occur.
However, such rapid replication creates an immediately detectable thermal signature enabling effective defensive policing instrumentalities to be promptly deployed before significant damage to the ecology can occur.
As an estimate of how long it would take the world to respond effectively to a novel threat, that seems extremely optimistic.
I wouldn’t expect humanity to be much better at responding to “nanoreplicators” than to global warming, with at least one major reason likely being the same — the growth of the existence and severity of the threat outpacing the growth of consensus among decision-makers about its existence and severity — and maybe other shared reasons, such as the problem technology’s becoming thoroughly embedded into national economies and individuals’ standards of living.
I just wanted to clarify the obvious mispaste of the time.
I find Kurzweil’s argument specious. He seems to argue for both the inevitability of self-replicating “biovorous replicators” and a global surveillance network that can scan for their “breakout” and respond to them. I mean, let’s say they “only” manage to consume the entire Amazon basin’s ecology before we manage to stop them. Problem solved, right?
I just wanted to clarify the obvious mispaste of the time.
Yes, my criticism was of the quoted passage from Kurzweil, not of your clarification; I apologize for not making that clearer.
Thanks! Sorry for my snippy tone. This entire sideshow (OMG! ChatGPT is soon sentient) is grinding my gears at the moment. But lobste.rs is not the place to vent about that.
Some years ago a randomart that I got looks like ascii art of a satellite dish:
+---[RSA 2048]----+ | o o+.| | E + ..++| | o . ..+=o| | + o. .*B.| | . =S +.oo=| | . . o B.oo| | . *.o..| | ... +oo. | | .....*B=. | +----[SHA256]-----+
And we’ll have much faster hardware,
That’s one of my biggest problem with the cloud providers. The hardware you get is so limited, you get so much more CPU and ram on a real machine. My ideal is still renting hardware: you don’t have to spend nights in the datacenter hanging boxes, but you do get powerful machines.
Whenever I look at the pricing for cloud stuff, it’s the storage that I find really difficult to swallow. I guess the reason is that it’s more difficult to move and impossible to over-provision but it’s still incredibly expensive.
You can buy a (reasonably good) 1 TB SSD for $80 right now, which is around $0.08/GB (and that’s not even the best $/GB). A place like DO will sell you storage at $0.10/GB per month, and there are providers which charge even more. Now, I know this is managed block storage, and you’re paying for the ability to scale your disk without copying everything over, but that’s a huge premium.
Yeah, at 100 times more expensive per month, even when factoring redundancy (let’s says x3) and multi-location (let’s say x5), it’s still 6 times as expensive, per month. The main cost I cannot easily compute is the host for the SSDs since they need to be attached to the same machine but at such prices, either someone could come and plug the SSD, or they could actually pay a huge machine with only the storage costs.
It seems hey had S3 (not the same performance as local SSD) at something like 1M for 8PB, which means each terabyte would cost 125k. It’s more reasonable at only 10 times more expensive per year than a raw disk. I’m not sure low volumes pricing for S3 is the same however.
Power to run things costs too. My (extremely generous to DO) calculations suggest each terabyte SSD could cost them $5 / mo to run (of the $100 / mo they bill it out at).
For me it’s egress costs. It’s insane. Quoting myself from the bird site:
“Reminder that for an on-demand t4g.nano instance on AWS, the cost of 3TB/month of egress traffic to the internet is 100x the cost of the compute”
~$2.5 for compute, $250 for egress.
You’re not even kidding. That’s incredible. Absolutely bonkers. A datacenter near me offers a 10gbps unmetered upgrade for $200/mo, which I know is on the cheap end, but still.
And 1Mbps billed at the 95th percentile should be around 1€/month now (at most). For 3TB you’d need 10Mbps, which means around 10€ per month. Bandwidth in Australia seems much more expensive (20x), maybe at 200€ per month. But I’m sure AWS already bills Australian bandwidth at Australia prices.
I’m seeing other figures which put costs of 100Mbps at 50 GBP and 1Gbps at 300 GBP. I doubt Amazon still counts in Mbps.
The big cloud providers offer instances up to around 64 cores with over 1 TiB of RAM (and up to 4 high end GPUs). You can buy faster machines, but few people do (or need to).
I don’t know, man. All this AI makes me feel incredibly stupid and generally unskilled. Every time the AI just solves something effortlessly the only conclusion tIhst comes to mind is how pointless learning that thing is now because the computer can do it on it’s own. I should’ve gotten a degree in marketing or psychiatry. At least the client in those is always human.
Once the AI has enough purchasing power do you really think we will be selling to Humans anymore?
I agree. Alternatively, even if human skill will still be required to review AI generated code, trawling through endless AI PRs looking for bugs all day long doesn’t sound enticing at all.