mrob

I'm of the opinion that improved developer productivity has been a net negative for at least a decade. Regardless of my opinion of LLMs, I don't want it any easier for people to add more antifeatures and pointless changes.

Most books are printed in black and white too. How does that make it hard to see?

The art style is "semigraphics", not pixel art. See:

https://en.wikipedia.org/wiki/Semigraphics

https://en.wikipedia.org/wiki/ASCII_art

https://en.wikipedia.org/wiki/ANSI_art

Giving developers the ability to impose Comic Sans on the users is bad. Giving users the ability to make their own tasteless choices is good. It's my computer and I'll make it ugly if I want to. Windows 3.1 included the famous "Hot Dog Stand" theme. The loss of this freedom only encourages user-hostile practices.

Agreed. Note the increased spacing to separate the generic "Help" button from the others that are specific to the dialog box. Aligning the buttons to the text input fields would break this separation and it could also give the false impression that the buttons were related to the input fields.

Considering trends in CVEs, printing is only growing importance. Printing has the unique advantage of giving you a record of data that's durable, unhackable, and possible to read without computers. If you print something, you can be confident that it's still going to be the same when you read it later.

Guns don't scale like drones. No matter how many guns you own, you can only shoot two at a time, and only one if you care about aim.

Building an autonomous drone swarm capable of nuclear-weapon-tier kill count is far easier than building a nuclear weapon. We already know how dangerous military drones are, and those are still mostly bottlenecked by relying on human-powered target identification. Building drones to indiscriminately kill unarmored civilians is an easier task.

Agreed. Anybody who thinks this is overreach should read this article:

https://www.lesswrong.com/posts/bGoo3NWzMAzsLQceJ/drone-wmds...

The important question now is finding out if it's the cannabinoids or the smoke inhalation. This study doesn't attempt to distinguish the two.

It doesn't matter. The proof verifier is traditional deterministic software with 0% hallucination rate, so any hallucinated proofs are easily removed.

>Indeed there are theorems that say the tool must malfunction at least sometimes.

Gödel's incompleteness theorem only states that there are true statements that can never be proved to be true. That limits what tools can do, but it's not a "malfunction". The exact same limitation applies to humans. A genuine malfunction would be if the tool "proved" a false statement to be true. That actually has happened before because of bugs in proof checkers, but software bugs can be found and fixed, and proof checkers are simple enough that it's possible to write many different implementations. It's extraordinarily unlikely that the same malfunction occurs in all of them.

There are many independent implementations of Lean's proof checker:

https://arena.lean-lang.org/

It's highly implausible that the same bug is present in all of them.

The exact meaning isn't important. The point is that something like RS-422 with the TX lines removed is perfectly adequate for receiving pricing updates. Anything more complex than that is adding unnecessary attack surface.

>Reduce power usage during peak electricity rates

This is the only one that requires remote write access, and only when "peak electricity rates" means a dynamic pricing system. But it doesn't actually need full Internet access. Instead, prices can be streamed via data diode to a local processor which calculates correct temperatures based on this information. This calculation should set reasonable limits on allowed temperature, so even if somebody sends false pricing information it's just going to waste some electricity and not destroy all the food.

>Optimize defrost cycles and compressor operation to save electricity

Assuming this means something different from "Reduce power usage during peak electricity rates", I don't see how it needs Internet access at all.

All the other points are monitoring tasks that can be done with read-only access via a separate data diode.

There's something very wrong with the electrical grid if they need to stagger startups over all the shops combined. Staggering startup within a single shop can be done with a LAN.

No amount of comparative advantage can help you when your economic values is less than the cost of keeping you alive.

Putin's getting old. If he dies before we hit recursive self-improvement, there's a chance some maniac gets access to the nukes and saves 4 billion of us (global nuclear war only kills about half of humanity).

The most straightforward method of eliminating all disease is to kill all life. This seems a much more likely outcome than the housecat scenario.

>no strategical impact by the actions of one player on the other

The players know if they're ahead or behind, which affects how much risk to take. Do you take the safe shot, or go for the tricky shot that could potentially save you a stroke if you get it right but could lose you more if you fail?

Comparative advantage only works when your economic value is greater than the cost of keeping you alive.

It's not unique. I for one agree. Mathematics is obfuscated because mathematicians prioritize compactness on the page over ease of understanding. This results in confusing notation (single-character variable names, implicit multiplication, implicit parentheses) and large numbers of omitted steps.

If I want to understand some mathematics, my first step is always translating it to code. Modern code (excluding array languages) no longer has a culture of minimizing character count, and omitting "obvious" steps is not possible. LLMs are based on an architecture (transformers) that was originally designed for natural language translation, so it doesn't surprise me that they're good at this.

That's no consolation to all the people they're going to kill with them.

>my browser does that every time I visit a site

The purpose of a browser is to make network requests. If I use a browser, I am implicitly giving it consent to make the network requests necessary for the web browsing I do.

This implied consent does not cover unnecessary requests, e.g. the adverts Firefox displays on new tabs by default are unacceptable, because I did not consent to them being downloaded. It also does not cover the network requests made by opening the "Extensions and Themes" menu, because merely looking at a configuration menu does not imply consent to make network requests.

But that fact that modern web browsers are a privacy disaster does not excuse bad behavior from other software.

No matter how you encrypt the data, transmitting it unavoidably leaks the fact that you're running software that transmits that data. There's no way to mathematically prove this is harmless, because there's no way to know how that information could be used against in the future in ways you didn't predict.

No software should ever make network requests without your consent.

Lean's proof checker is reproducible, and has been independently reproduced several times. See:

https://arena.lean-lang.org/

>In order to trust it a formal verification is not enough unless it is human understandable.

The whole point of formal verification is to remove the necessity of understanding most of the work. We only need to trust the formalization of the problem statement, the proof verifier, and the formalization of the result. We already have proof verifiers that humans understand to a high level, and the formalizations of the problem statement and the result are much simpler than the full proof.

I'm confident that the Navier-Stokes equations can blow up because I'm confident that Lean works correctly, and I'm confident that the mathematicians verified the problem statement and result correctly. This is despite the actual proof not being human verified yet (as far as I know), and despite the "human-readable" version not actually corresponding to the formal proof. The formal method still worked.

>optimizes the keys for either reachability

It doesn't because it only has a single row of keys. Piano music is full of awkward finger crossings that could be avoided with multiple rows of keys like on the Jankó keyboard.

>or feeling

You can texture or raise/lower the keys on any keyboard as you please. No layout has an advantage here.

>the range for one hand is smaller than the guitar's

True, but the traditional keyboard is even worse.

>there's no bending/sliding/vibrato

Exactly the same as a traditional keyboard.

>it very quickly learns to work on "it's on adjacent lines therefore it's a third apart"

The problem is "a third apart" means different things depending on where on the diatonic scale that third is. What I actually care about is how many MIDI note numbers apart it is, because that's what corresponds to the finger positions on the instrument.

>G# and Ab aren't even played the same on some instruments

Seeing as we've freed up the sharp and flat symbols, we can repurpose them to mean adjustments by whichever comma is relevant.

>Light bulbs got 6x as efficient and roughly nobody wants 6x as much light.

I want more than 6x as much light as I had in the incandescent bulb era. Indoor lighting is usually very dim compared to outdoor lighting, and that makes it harder to see things. As I get older and my eyes degrade I expect I'll want even more light. People running offices understand this and provide more lighting than typical for homes. See:

https://en.wikipedia.org/wiki/Lux

1-indexing in music is as much a mistake as 1-indexing in programming languages. The traditional interval names are mostly 1-indexed too, which just adds pointless complexity you have to compensate for whenever you're adding or subtracting. Only exception I can think of is the tritone, which is inconsistently 0-indexed (and in a different scale).

It's IMO crazy that going up seven scale degrees makes an "octave".

>They are not two different clefs, the are two halves of the same 11-line staff.

This is actually another reason to use an isomorphic/"chromatic" staff. If you prioritize data compression (traditional notation), you have 7 notes per octave + modifiers. If you prioritize linearity (isomorphic/"chromatic" notation), you have 12 notes per octave.

12 is an even number, meaning you can stack octaves and have consistent notation for each one. With traditional notation, you always have to keep track of which octave you're reading and adjust accordingly.