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

> They already did

Yes, but they don't and won't too (at least until they do again)

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.

> Even alternatives like GrapheneOS relies on AOSP

There are alternatives that don’t: Mobian, Ubuntu Touch, PureOS, postmarketOS, Sailfish OS.

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.

GrapheneOS supports remote attestation, but banks have to add the fingerprint of the official GrapheneOS verified boot keys:

https://grapheneos.org/articles/attestation-compatibility-gu...

Some banks even do.

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.