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

--and Bing, Brave, DuckDuckGo, Ecosia, SearXNG, Startpage, Yahoo! JAPAN, Yandex - and Kagi.

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