aleks224

There's a quote in the bible that says something similar:

"Verily, verily, I say unto you, Except a corn of wheat fall into the ground and die, it abideth alone: but if it die, it bringeth forth much fruit.”

(John 12:24)

This blog post exposes the badness of SMS-based recovery. I think other recovery options such as Yubikey aren't ideal either, as a Yubikey may simply stop working and you're completely locked out. The specific situation the author of the blog post isn't dramatic - he can't receive SMS - personal decision to avoid roaming charges.

But in all seriousness, if there's an authentication recovery standard, it should serve all people including those who are in seriously difficult circumstances (e.g. homeless or ill). The question then is what should recovery look like in those cases.

To me it looks like good old recovery code on paper is the best solution, as it doesn't depend on ever-changing device ports, or hardware malfunction due to lack of use long-term (such as 10-15 years).

I wonder whether authentication apps nowdays address that aspect and make and I kinda doubt so (i.e. can you print out a QR code with all account information in your typical TOTP app?).

Do TOTP authentication apps typically provide recovery codes option? Can they squash all of the added TOTP codes you have in the app into one code?

For a set of primitive operations (such as those in Turing machine), how can you be sure that it spans all possible computations? It sounds that's one of the challenges Turing had - so he went at lengths to show that by various "soft arguments", e.g. that it's possible to build a VM (Turing machine that runs other Turing machines IIRC). Later on, it was shown that the Turing machine is equivalent to machines other folks came up with (Goedel's recursive functions, lambda calculus, etc) and a consensus emerged that they are all describing a full set of computations.

>The only way to mitigate this is to use computer-readable proofs, which can be verified by algorithms to ensure correctness.

This seems like a strong overstatement. We got by for more than 2000 years without computer-readable proofs, relying on intuition and validation.

Very interesting! My understanding is that you're thinking about this more in terms of an 'application environment for power-users' than in terms of a 'multi-faceted IDE with lensing'.

To clarify, the specificity of Emacs is that it fully exposes it's internal function sets to the world. This could be done by other applications in an organized way. For example, in the picture-editing app example, it would amount to allowing scripting over the features that the app exposes. The scripting feature would come from the environment, not from anything specific the app itself does (apart from being built in that environment). The previously mentioned IDE could then be thought of simply the multi-tasking environment in which such generic applications are running.

Does this roughly correspond to what the project is about?

If I'm understanding this correctly, with your Lisp IDE you could have an image sub-editor which may expose functions for image modification (eg. cropping), which could be called from the parent-editor. Is this accurate?

Also, what is it about Lisp specifically that makes it suitable for this undertaking?

> A trisector is a person who has, he thinks, succeeded in dividing any angle in three equal parts using straightedge and compass alone. He comes when he sends you his trisection in the mail and asks your opinion, or (worse) calls you to discuss his work, or (worse still) shows up in person.