IngoBlechschmid

I agree! Martín Escardó never tires to say that he uses the Agda proof assistant in exactly this sense, as a kind of interactive blackboard for taking notes and structuring his thoughts. The vast TypeTopology repository is the result of years of following this philosophy: https://github.com/martinescardo/TypeTopology

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.

Strongly depends on the subbubble of mathematics. In some parts of type theory / formal proofs for instance, there is a rather strong rejection of LLMs (for moral reasons in addition to quality reasons). The proof assistant Agda was even forked for this reason: https://types.pl/@amy/116522250630340534

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

> So hibernating is really the only proper way to protect against cold boot.

I agree; or resurrecting FridgeLock: https://www.sec.in.tum.de/i20/publications/fridgelock-preven...

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.

Several options. One is you restart and boot from a live system where you are root, and then dump all memory. This is described in the paper with the witty title "Lest We Remember: Cold Boot Attacks on Encryption Keys":

https://www.usenix.org/legacy/event/sec08/tech/full_papers/h...

Other options: DMA attacks. Also you never know what the Intel Management Engine hidden in your computer is doing. It's running a version of Minix you don't have any control over, and it has full access to memory.

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

Right! Which is why integration tests for these kinds of features are all the more important.

It was also fun to write, and enabled git-bisecting to isolate the specific kernel refactoring which introduced this bug: https://github.com/NixOS/nixpkgs/pull/532499

Qubes OS, the Linux distribution aspiring to offer a reasonably secure operating system, pioneering a "every app runs in a virtual machine" approach in the Linux laptop/desktop space, tracks this at the following issue:

https://github.com/QubesOS/qubes-issues/issues/2890

Okay, yes, sure. It definitely is the most-used encryption software for Windows.

But I would never trust it a second, being proprietary and known for issues. You likely know that, but for the benefit of others:

38C3 - Windows BitLocker: Screwed without a Screwdriver https://media.ccc.de/v/38c3-windows-bitlocker-screwed-withou... https://www.youtube.com/watch?v=5eNtT2p12cM

Oh, which one is it?

(You don't mean BitLocker, right?)

Suspend to (encrypted) swap might be a good middle ground between you and grandparent. Suspend to memory will (at best) protect your LUKS volume key, but other sensitive data remains.

A couple of years ago, three security researchers from the TU Munich implemented a prototype for also encrypting (most) parts of the memory just before suspend, to address this limitation; but as far as I know, it was not upstreamed or developed further: https://www.sec.in.tum.de/i20/publications/fridgelock-preven...

Yes, if you simply suspend your laptop on most stock Linux distributions, then everything including the master key is still kept in memory. But Debian pioneered the (optional) cryptsetup-suspend addon. This issues a luksSuspend command which is supposed to wipe the key from memory, and on resume asks you to resupply your passphrase.

Up to kernel 6.8, this worked as described; starting with kernel 6.9, it silently didn't.

An interesting example is the Dhall language: https://dhall-lang.org/

It is a configuration language with general programming features, but it is decidedly _not_ Turing complete. It seems to sit at a sweet spot between "just JSON, no programming convenience at all" and "full-blown programming language with nontrivial toolchain".

Just a tiny addition: Yes, N log N is the average time, but the distribution is heavily long-tailed, the variance is quite high, so in many instances it might take quite some time till every item has been visited (in contrast to merely most items).

The keyword to look up more details is "coupon collector's problem".

A good friend of mine was recently sentenced to prison for publicly using this kind of phrase during a protest for climate justice. When Germany's equivalent of the Supreme Court, the Bundesverfassungsgericht, learned of this case, the court immediately ordered their release and declared the original verdict void: According to the Bundesverfassungsgericht, (in the specific situation at hand) this phrase is more a value judgment and less a factual claim.

Together with a fellow activist, who also served as informal legal counsel, they gave a talk on this case at the 38th Chaos Communication Congress: https://www.youtube.com/watch?v=r5RmTOGucZo

Somebody asked in a now-deleted comment: 'Right, and what does it mean in the context of "A monad is just a monoid in the category of endofunctors"?'

Here is an answer to this question:

What the parent poster referred to are "monoids in the category of sets". You can recognize this as they have introduced the carrier as (just a) set.

But the notion can be generalized. For instance, a "monoid in the category of datatypes" would not be given by a mathematical set and a mathematical binary operation, but by a datatype and a computable binary operation. (To make this precise, I would need to fix which "category of datatypes" I have in mind. It could be the category of Haskell types and Haskell functions, for instance; but C types and functions would work just as well. I could also go all the way to the effective topos, which contains lots of types which most mainstream programming languages are missing such as true quotient types.)

Finally, a "monoid in the category of endofunctors" is given by an endofunctor and a natural transformation. Endofunctors can be pictured as container kinds (e.g. ordered lists, unordered lists, Maybe/Optional, trees, vectors of length n, pairs, ...) and the additional datum of the natural transformation is what singles out those container kinds which support a "flattening operation" from those which don't. For instance, we can flatten a list of lists into one (long) list, but we cannot flatten a pair of pairs into one pair (we would need to drop two of the four elements).

Just as it is quite convenient that many results about integers or lists also hold for all monoids in the category of sets, it is quite nice that many results about monoids in the category of sets also hold for all monoids in all categories and hence in particular to monads.

Gwern has an interesting take on this: https://gwern.net/cyoa By pivoting to "choose your own adventure"-style games, multiple issues (quality, costs) might be resolved.

The paper was originally released in April 2023, it just got version-bumped a couple months ago :-)

Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.

There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.

This set of slides, originally devised for the Chaos Communication Congress, might be helpful: https://www.speicherleck.de/iblech/stuff/ac-38c3.pdf

- Precise statement of the axiom

- Overview of its consequences

- A counterexample (in an alternative universe)

- Consistency of the axiom

- Gödel's sandbox for containing the axiom

I like Vim's digraphs, which go in a similar direction. For instance, Ctrl-K = > gives ⇒, Ctrl-K a * gives α. An overview of available digraphs is available at :digraphs.

Otherwise I like the Agda input method of Emacs, where \to gives ⇒ and \alpha (or \Ga) gives α.

I'm currently creating an interactive tutorial on Agda, with lots of embedded exercises (running purely in the browser/on a server, no installation required), perhaps it is useful to some:

https://lets-play-agda.quasicoherent.io/

> speaking of climate change, global overpopulation kinda has an impact on it!

You are right, of course; but just to put some perspective to it:

If Thanos-style the population and the CO2 emissions would be cut in half, this would not be enough at all -- we need to get back to 350 ppm (or similar).

I'm writing this to counter the meme that "climate change is Africa's fault, because of their population count".