IngoBlechschmid

The Curry-Howard correspondence.

For instance, in mathematics, we have A ⇒ A (every statement implies itself, for instance "if it rains, then it rains"); and analogously, in programming, we have the identity function of type A → A (which reads a value as input and outputs the same value).

This is the tip of an enormous iceberg identifying, in a certain precise sense, proving with programming (and stating mathematical assertions with specifying the desired behavior of a program).

However, programming is a bit more general than proving: Circular proofs are simply of no value, whereas looping programs can still be valuable. For instance, I for sure hope that the main loop of the browser I'm currently using to fill out this textbox does not prematurely stop.

> Of course Lean proofs are rarely a good way to understand proofs, but hopefully they can be used to generate more human understandable arguments.

I would object to the first part: Of course there is a nontrivial learning curve, but then I'd argue that non-slop Lean/Agda/Rocq/... formalizations are amazing for understanding proofs. A good formalization presents the outline and the key arguments in nicely structured form, and then, unlike pen-and-paper proofs, also allow you to get the details on every single step, exactly to your desired level of depth.

The proofs in Martín Escardó's TypeTopology Agda repository come immediately to my mind as an example. [An interactive Agda tutorial is here: lets-play-agda.quasicoherent.io]

In contrast, LLM-generated formalizations can currently be extremely messy. They certify truth and can also contain interesting arguments, but substantial work is required to bring them into a shape that contributes to the actual goal of improving our understanding of the mathematical landscape.

> If I defined some pointless construction and it turned out to be very difficult to prove, it would absolutely and automatically over time be considered a "high utility" problem (again, for some odd reason).

Yes and no.

No: There are lots of very hard open problems which are judged to be of little value by mathematicians and hence garner little attention.

Yes: If a conjecture resists proof for a long time, this can indicate that we still have a substantial gap in our understanding. We project utility into an eventual closure of this gap, not into the statement of the concrete conjecture at hand. The gain in understanding is what we actually work for. It just turns out that chasing specific results, even if they are mostly dead ends on their own, is useful for orientation.

The (by now solved) problem by Fermat (for all integers a ≥ 1, b ≥ 1, c ≥ 1, n ≥ 3, the equation aⁿ + bⁿ = cⁿ does not hold) and the (still open) Collatz conjecture are perhaps good illustrations of this situation.

It's kinda both, right? In any case, good clarification, thank you.

> Can I ask one question? Why not use hibernation at that point?

The sibling post by cyphar gives a good reason; while UEFI Secure Boot has its own share of issues, it can be a valuable ingredient in defending against evil maid attacks.

But another reason is... convenience. Resuming from RAM is faster than resuming from disk, especially so if your "disk" is actually just a USB flash drive. I know that it might be a bit weird to ask for convenience when the motivation is security. But I argue that there are use cases where the tradeoff is sound.

With hibernation, all your data is safe but the inconvenience might seduce you not to use it.

With suspend to RAM and your distro's version of cryptsetup-suspend (and the kernel patch or alternatively the cryptsetup workaround), only your volume key (and hence the bulk of your data, potentially terabytes worth of sensitive information) is safe, but sensitive data in memory (recent files, recent chat messages, session cookies, ...) is not. But on the other hand it's quick.

Some people use a combination: suspend to RAM for short breaks, where they expect to remain physically able to fully switch off the laptop when something happens; and suspend to disk for longer breaks.

It all depends on your threat model.

No, it is indeed a kernel bug in the code path responsible for luksOpen.

Debian (and the distributions which ported cryptsetup-suspend) relied on cryptsetup luksSuspend doing its thing correctly, and cryptsetup luksSuspend relied on cryptsetup luksOpen doing its thing correctly, and cryptsetup luksOpen relied on the thread keyring being purged from memory on process exit, which is promised in the tread-keyring(7) manpage.

Yes, you are right: LUKS encryption protests your data at rest. An attacker which steals your disk can only gain little, like the information that you have used LUKS (unless you put your LUKS headers elsewhere, separated from the disk) and perhaps disk and disk sector usage statistics.

Sorry, aimed for a technically precise title and didn't want to bait clicks.

Yes, this does not affect people on stock configurations for the plain reason that they wouldn't expect the volume key to be safe during suspend anyway.

Debian's solution was ported to several (most?) other distributions and I guess quite a few people maintained private ports.

The thread-keyring(7) manpage promises: "A thread keyring is destroyed when the thread that refers to it terminates." For their key upload (from userspace to kernelspace) mechanism, the cryptsetup project relied on this property; but kernel 6.9 introduced a regression invalidating this property.

Exactly. Cryptsetup wouldn't know about the extra copy of the volume key in kernel memory. Which is why, dramatically, it appeared secure ("surely I wouldn't be asked to resupply the passphrase if the volume key is still in memory, right?").