Noam Postavsky

I wrote a library that lets you cycle through the available themes in Emacs. F10 and shift-F10 keys will cycle forward and backward through the themes. The theme name is printed for reference.

https://github.com/tsengf/theme-cycle

Installation
Download theme-cycle.el into ~/.emacs.d.

Add the following to your Emacs configuration

(add-to-list 'load-path (expand-file-name "~/.emacs.d)
(require 'theme-cycle)
;; Load as many themes as you are interested in exploring.
(use-package doom-themes)
(use-package ef-themes)
(use-package modus-themes)
(use-package solarized-themes)

To Use

Use F10 to cycle forward through the themes. Use shift-F10 to cycle backward through the themes.

It is also true that computers with CHOOSE can rather trivially produce outputs for which there is no corresponding classical TM implementation. This is what is obscured in proofs that NDTM == TM.

I want to focus just on this one claim since the rest seems to follow from this. Apologies if you've already addressed this elsewhere here, but the other threads are hard to follow given finite time. I agree that having non-deterministic choice makes some programs trivial, like a program P that produces a random bit string. For any given bit string B of length N produced by CHOOSE, it seems trivially true that there exists a Turing machine T that can also produce B using input shorter than N. I don't think you're disputing this claim, which is one way of looking at equivalence. The only comparison I can think of that escapes equivalence, is if we further require that T be bisimilar to P for any random set of output lengths N. I don't think that any single T can satisfy this form of equivalence, even if there exists a T that can simulate any specific, finite set of output lengths. Is this the equivalence relation you're suggesting under which NDTM != TM? If so, is this actually a meaningful equivalence failure? Just because they aren't bisimilar doesn't mean they aren't equivalent in every other way that matters.

Counterexamples in Type Systems

The "counterexamples" here are programs that go wrong in ways that should be impossible: corrupt memory in Rust, produce a ClassCastException in cast-free Java, segfault in Haskell, and so on. This book is a collection of such counterexamples, each with some explanation of what went wrong and references to the languages or systems in which the problem occurred.