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.

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.

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.

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

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

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.

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.

- memory/yyyy-mm-dd.md

- MEMORY.md

- SOUL.md

> 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.

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.

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.

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".

The inverse is also difficult. Pick a random 15 second movie clip, how to describe it using text without losing much of its essence? Or can one really port a random game into a text version? Can a pilot fly a plane with text-based instrument panel?

Text is not a superset of all communication media. They are just different.

The program used to check the validity of a proof is called a kernel. It just need to check one step at a time and the possible steps can be taken are just basic logic rules. People can gain more confidence on its validity by:

- Reading it very carefully (doable since it's very small)

- Having multiple independent implementations and compare the results

- Proving it in some meta-theory. Here the result is not correctness per se, but relative consistency. (Although it can be argued all other points are about relative consistency as well.)