crvdgc

This is like the mirror image of the popular Chinese content of picking a few homeless scenes of the US and painting the whole image of US life experience from it.

Obviously, the author has deep engagement with the Chinese internet culture (the "junk food" part that I would avert), but the over generalization is comical.

Or maybe that's the point? The author is trying to be provocative? For someone with zero background of the Chinese internet culture, this could be a starting point (although an extreme one), but don't take this to represent the whole reality.

One example, the quoted book review of Three Body Problem draws the complete opposite conclusion that the aliens are Chinese. To anyone with actual Chinese culture context, they are obviously "Westerners".

<spoilers>

- Far more advanced technologies.

- The Trisolarians cannot lie, so that becomes the only advantage of humanity. -> Art of War

- The Trisolarians are blocking physical experiments to stop science and technology advancement. -> Entity list and export control. Huawei.

- The factions in human that supports the invasion. -> Evans hated humanity because of The Silent Spring, which is supposed to represent the Western self-guilt culture.

- The emaciated generation that failed at launching the mutually assured destruction device is an image of "Westernized" generation.

The overarching background of the book is a discussion of which direction that China should take after 1989 stopped the democratization process and drove the Western powers into hostility. The author Cixin Liu has a more or less social darwinism answer for that ("Dark Forest"). Not that he endorsed social darwinism, but that's the main theme of the book.

</spoilers>

To be fair, if the two words indeed don't appear in either the webpage or the codebase, it is a bit strange. It's like implementing a whole Google alternative without ever using the words "search engine".

A video of the launch and landing: https://www.youtube.com/watch?v=IcnebC7xva4

In Morocco?

My guess would be the version number tracks the architecture change, not the weight change.

For the sake of argument, let's assume everything in the post is agreed upon, does this mean

1. They'll open source the alignment technology? For open weight models, it's the only possible way to pass the safety without an external guardrail triggering system (which would be the same to open and closed weight models).

2. They'll allow others (including CCP) to define part of the safety test? Otherwise, I can't imagine how the CCP would be onboard.

3. A "western" model passing the safety test can be trained with distillation? Or is that a "distillation attack" as well?

Even if that's the case, the tragedy should have been disclosed reponsibily.

The fact that the parents had to make further efforts to go through their daughters death to warn others just feels wrong.

Thank you. Video from the thread: https://www.youtube.com/watch?v=x9XDsiG40Uk

(comment itself: https://www.reddit.com/r/space/comments/1usdigz/comment/owna...)

That language should be called Fusion and this language Fission.

Some providers in the UK issue debit cards with limited interest-free overdraft and charge back features. So they are basically credit cards if you squint your eyes enough.

Vision has been in A/B testing for a while now (at least in China). Is there an official announcement that this will be available for everyone?

Nix also needs the build output to be deterministic to calculate the hash. It also has the problems of timestamps etc. The build environment tries to be hermetic by setting the time to be epoch among other things.

In his later years (late 1980s), he also advocated for AI and human superpower research.

The superpower thing turned out to be pseudoscience later. As a result of being lumped together, for a long period of time, AI was regarded as pseudoscience in China as well.

Although to be fair, during the same period, the US and the USSR were researching superpowers as well.

While in Japan, I heard an urban legend that, it typically takes 5 accumulated years for a foreigner to acquire hay fever in Japan.

In the long term, the biggest problem is that space data centers are very hard to defend against missiles.

Another angle is that most donations to Linux kernel are in the form of paid employees doing kernel work. I wonder how much the kernel need besides that.

comptime is a restricted form of dependent typing.

In addition to the normal value to value, type to type, and type to value functions, in comptime, you can write static value to type functions.

In full dependent type, you can in addition write dynamic value to type functions, completing the value to type corner.

So in terms of typing strength, plain Haskell < Zig < dependent type languages.

I didn't find anything particular, but in general it should apply to anyone under the jurisdiction. I think it's illegal to drink underage in the US, even if the person is a tourist and they are allowed to drink by their own country's law.

Unfortunately, the discussion focused on the somewhat click baity title "proved this program correct". It's unclear what "this program" is. If it refers to the core algorithm with a proof, then there's no bug. If it includes the runtime and the header parser, then Lean didn't prove it correct.

That being said, using a coding agent to direct fuzzying and find bugs in the Lean kernel implementation is the big news here. (After all the kernel's implementation is not proved.)

The moral of the story is to push for more verified code not less and try AI bug hunting.

For what it worth, there's uBlacklist for Google.

https://ublacklist.github.io/docs/getting-started

Sovereign AI adds another layer of meaning now that sovereignties are at war.

> GitHub does not and does not plan to include advertisements in GitHub

They already did! https://github.com/orgs/community/discussions/65245

People, we just solved the LLM watermarking problem.

Even alternatives like GrapheneOS relies on AOSP. I wonder if it's possible for regulators in certain countries to pressure Google to kill it in the future.

Even if that's not the case, I'd imagine attestation apps like banking apps would require some kind of identity verification in exchange for trusting Graphene's keys.

In principle it doesn't make sense to leave any escape hatch, but I guess as always, it boils down to economy.

In theory, it's possible to have a third party (other than Google or Apple) to provide attestation on third party hardware.

You can have a separate core and kernel to run such code. They don't have to be powerful, but they'll need to be small enough to be verified by the said provider. For most of the code that doesn't need attestation, they can be executed on normal hardware.

The provider also has to convince the regulator or banks to trust them. However, if that's solved, the user should feel no difference between pure Android and alternative platform plus attestation.

How long before people realize that they too have limited context length and adopt:

- memory/yyyy-mm-dd.md

- MEMORY.md

- SOUL.md

At least for this article it's more about the job, or to be precise, the past where job and passion coincided:

> Ultimately if you have a mortgage and a car payment and a family you love, you’re going to make your decision.

Nothing is preventing the author from continuing to write code by hand and enjoy it. The difference is that people won't necessarily pay for it.

The old way was really incredible (and worth mourning), considering in other industries, how many people can only enjoy what they do outside of work.

Among the six patterns identified, it's interesting that "Iterative AI Debugging" takes more time (and possibly tokens) but results in worse scores than letting AI do everything. So this part really should be handed over to agent loops.

The three high score patterns are interesting as well. "Conceptual Inquiry" actually results in less time and doesn't improve the score than the other two, which is quite surprising to me.

Some valid points, but I hope the authors had developed them more.

On the semantic gap between the original software and its representation in the ITP, program extraction like in Rocq probably deserves some discussion, where the software is written natively in the ITP and you have to prove the extraction itself sound. For example, Meta Rocq did this for Rocq.

For the how far down the stack problem, there are some efforts from https://deepspec.org/, but it's inherently a difficult problem and often gets less love than the lab environment projects.

This specific example to me is less likely a consequence of model collapsing, but the "personality" adjustment about how aggressively it should read into the user's intention.

From time to time, I enjoy the model guessing what I meant rather than what I wrote. For example, "Find the backend.py" can be auto-corrected into "find the app.py".