est31

By similar i meant the strong and powerful type system that Rust has, plus its safety guarantees (iterator invalidation is a compiler error etc). That is in the end a proof system: you are proving to the compiler that you really don't mutate the buffer and you can't drop the T in &T, etc.

Of course the Rust language doesn't give you tools to prove that the program is bug-free or such. The proofs only extend to a basic set of properties, but there is a proof system in Rust.

As for other ML languages, they aren't really C/C++ competitors performance wise, Rust is.

Also you would probably want to cache the compiler's output in git because running that compiler would take a long time, and you probably want the compiler's output to still be inspectable to human inspection. In the end that compiled artifact would look a lot like source code.

I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).

Which models do you see to be productive for the task of writing lean? Big fan of pgrust.

I recently assembled some IKEA furniture and wow it was so fun. It was the same feeling that I had back when I was manually typing out code.

Now I prompt LLMs all day for my job and it is much different. Yes, AI allows me to write way more than in the pre-AI age, but it is certainly fun in a different way, not the kind of IKEA-assembly fun.

The hype will be over one day, but when is that?

I've done multiple life choices, away from AI, believing it to be a hype, but this hype is still growing, still not dying.

Both in 2019, as well as in 2023, i.e. not 2 or 3 months ago.

The plutonomy transition is well under way. The sardinian seafront villa will likely retain and gain value as the early anthropic employee might like it, while the house in some flyover state might not find any buyers.

The economy of the future will be about yachts, supercars, hermes bags, private air travel and ozempic. Not about how you made it possible for everyone to watch a gigantic library of videos for free, or how you made cars affordable for everyone.

I doubt that if Norway buys OpenAI, it will be the company that captures the value.

There is no inherent property to those model makers that they will capture the value of the AI boom. The model companies have a lot of competition from chinese models. Of course the US government will likely still keep some model makers alive (just alone for DOD supply chain reasons), but the chinese models will certainly compress margins.

It might as well be a chipmaker, a power company or a cobalt mining company.

Ultimately, it's up to the US government to decide if OpenAI can capture the value provided by AI: if chinese models get banned from the F500, then maybe one of america's famous duopolies can establish themselves.

But this hinges on congress mostly to pass certain laws to put OpenAI into that position. But which value does congress have? If OpenAI is owned by a bunch of Forbes 400 people like right now, then of course those will lobby the hell out of congress and ensure their stakes in OpenAI make them extremely rich.

But Norway doesn't have that access to lawmakers, they would see it as external influence by an alien power. They can certainly benefit from this trend though by being a shareholder.

To give a concrete example of the US government making life hard for foreign investors, take the T-mobile and sprint merger. T-mobile is majority owned by Deutsche Telekom AG, whose biggest shareholder are various institutions of the german federal government.

In this case, the US government just had to _approve_ the purchase, something very standard that happens all the time, but they still dragged that approval out as long as possible, even though Germany is a fellow NATO country.

I think it's partially for responsibility reasons. Your employee approved the bash call? not our fault then!

Yeah with China pumping state subventions into car manufacturing, they can outcompete any car manufacturer anywhere in the world. The leading battery technology is in Asia anyways.

The German car industry will not die completely, as the EU can protect its market from chinese manufacturers through regulation. But it will shrink and transform. Probably also back to fossil fuels (yuck), because there the Germans still have a lead (they are trailing with EVs).

Germany's new hot industry is defense technology.

cargo check is useful to verify the code compiles (it's extremely rare to have compilation errors that survive cargo check). But cargo build is required if you want to actually try out the code you wrote, e.g. in order to run a test that you or the LLM wrote.

Is it the AI companies though that will capture the value that AI creates, or will it be the still-private startups, or new to-be-founded startups altogether?

Startups are taking longer and longer to reach public markets, so more and more value creation requires you to be a family office, angel, or hedge fund.