MaxRegret

Is your position that the term "proof by contradiction" should not be limited to proofs of ¬¬P followed by double negation elimination, and should instead also encompass proofs of ¬P that start with "suppose P, for contradiction"? I agree that this is in keeping with traditional usage.

But I think Andrej Bauer's distinction is hardly unique to him (and I probably first encountered it from a different source). It's simply a way to square two widely-held beliefs, even amongst professional mathematicians (in my experience):

1. Intuitionistic logic does not admit proof by contradiction. 2. The proof that √2 is irrational requires proof by contradiction, and therefore is not intuitionistically valid.

I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive. This is in line with what Bridges says in your link.

The other alternative would be to more narrowly redefine "proof by contradiction" so that it does not apply to the proof of the irrationality of √2. I happen to prefer this because its simplicity appeals to me, but this is a matter of taste and admittedly hard to defend. I've also made peace with the idea that terminology is fluid and can have somewhat varying meanings for different communities and across time.

I think if someone understands the topic well enough to have the discussion we're having, they're unlikely to have the misconception we're talking about. So in that sense, we're engaging in a bit of pedantry.

To be fair, one doesn't need a deep knowledge of the "discipline proper" to realize this. If you're considering the field to be intuitionistic logic or constructive mathematics, I would readily admit that I have a superficial knowledge. If you consider the "discipline" to be mathematics broadly, even this level of knowledge is actually quite uncommon.

Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth, rather than a reasonable view of what a proof by contradiction is?

I agree with what you say about mathematicians, being in an adjacent field myself. However, most mathematicians are not logicians, and we are seldom careful about making distinctions that only matter in non-classical logics. I do think that this particular distinction (between proving negation vs. proving the negation of a negation) is worth making, though.

Even if we are, as a matter of practice, used to invoking the law of the excluded middle without a second thought, I think it's good to keep in mind in which proofs it is actually required and where it is not. So, for example, and to the GP's point, proving ¬Q ⇒ ¬P by proving P ⇒ Q doesn't require LEM, but the converse does.

The trouble is that when translating mathematics to logic, it's often not clear what is a negation and what isn't. Is "x is irrational" the sentence ¬P for P being "x is rational" or is it simply an atomic sentence on its own? One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians.

Also, proving ¬P by assuming P and deriving a contradiction is not "proof by contradiction"! That is just how you prove negations — ¬P is often taken to be syntax sugar for P ⇒ False.

It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction. Technically, what you've actually done is proven ¬(¬P). Now if you're a classical logician, you would say that ¬(¬P) is equivalent to P; if you're a constructivist, you wouldn't.

So proof by contradiction isn't in the constructivist's toolbox, with the proviso that many people think they're doing a proof by contradiction when they're not actually.

You probably know this already, but the problem isn't remote desktop into a logged-in session (krdp supports this) but rather logging in remotely into a headless server without a local session running. This is slightly more complicated because the login manager has to get involved and present its UI remotely. This is what that bug is tracking.

If you're happy to use Gnome with GDM as the login manager, remote headless sessions are supported already with gnome-remote-desktop: https://gitlab.gnome.org/GNOME/gnome-remote-desktop#headless....

The things that "start going really wrong" are listed immediately after that quote, and have nothing to do with the drop-off trajectory. Epic had problems with the ground stations they were using to communicate with their spacecraft. One of the two stations was offline because of a power failure. Then they "discover[ed] an unlikely incompatibility between their transmissions and the ground station hardware."

On a ride share mission, the primary payload determines the target orbit. If Intuitive Machines decides they want to go to a different orbit, then Epic has to deal with it. But they will be told this well before launch, with enough time to plan how many trajectory change maneuvers they need.

But even though they know beforehand how many burns they'll need, their exact parameters have to be calculated after launch once SpaceX uses the rocket's on-board guidance instruments to determine the actual insertion orbit. Usually this is within a few meters per second of the planned orbital velocity, but you need to know that last bit of error to figure out exactly how long the correction burns need to be. This doesn't change the overall maneuver plan, just the fine details.

The problem was that after launch, when SpaceX gave them the information they needed to calculate the burn parameters, they didn't have a working uplink to command their spacecraft to do the burn. So it just stayed on its original trajectory for longer than intended, getting more off-course the whole time.

Passkeys are a public/private keypair, where the service you're authenticating against has the public key and your browser has the private key. To authenticate, the browser demonstrates that it has the private key by signing and returning a challenge sent by the server.

So, unlike API keys, the actual passkey is never sent anywhere out of your device. Passkeys are more like SSH keys than API keys.

One difference between SSH and the WebAuthn protocol is that the challenge identifies which key it is expecting. So the user doesn't have to explicitly select which key to use.

It turns out the acidic environment in most beverages inverts the sucrose in cane sugar to form a 50:50 mix of fructose and glucose. In the end, the fructose/glucose ratio in cane-sugar-sweetened drinks becomes similar to high-fructose corn syrup, which is about 55:42. And the reaction is quick: about half the sucrose gets inverted in about three weeks. [1]

[1] https://www.youtube.com/watch?v=NY66qpMFOYo

In this case, multiplication by any nonzero fixed element of the ring is an injection from the ring to itself. Any injection from a finite set to itself is indeed a surjection (and so also a bijection).

Steve Mould just released a video about the microscopy technique that was used to capture this 3D relief of the painting: https://youtu.be/o-dZKBwbsis

Don't forget Pandoc!

Zotero has a beta Android app [1][2]. I haven't used it, so I don't know if any functionality is missing.

[1] https://play.google.com/store/apps/details?id=org.zotero.and... [2] https://forums.zotero.org/discussion/110371/available-for-be...

That's what C++ does because it has no way to ensure that you use the atomic reference counts in multi-threaded code. But, as the author writes in the blog post, Rust can in fact ensure this. So it lets you to use the more efficient non-atomic reference count for single-threaded use, saving the unnecessary cost of various memory access barriers.

Just because a language is designed for concurrent programming, it shouldn't make it impossible to achieve full single-threaded performance, as long as you're not compromising safety.

I remember flying VOR radials in Microsoft Flight Simulator 5.1, released in 1995. It came with a printed Pilot's Handbook [1] that included IFR procedures, explained how navaids work, and included various sectional charts.

[1] https://archive.org/details/microsoft-flight-simulator-v-5.0...

Desktop applications can continue to use the X11 protocol, but then they'll be talking to the Xwayland server, which in turn Wayland to actually draw its clients' windows on the screen.

But it's preferable to have applications directly use the Wayland protocol, which is what Firefox is experimenting with. For most applications, this is easy because they use some standard toolkit like GTK or Qt, which will transparently use Wayland without the application caring about it. But Firefox uses its own toolkit, so it's a bit more work.

You're right, the real problem with predicting trajectories through those "keyholes" [1] isn't solving the dynamics equations: our numerical integrators are more than good enough. The problem is we can't measure the initial states with enough precision.

[1] https://en.wikipedia.org/wiki/Gravitational_keyhole

Yes, indeed! The actual rate of heat transfer is equal to the temperature delta divided by the thermal resistivity of the body-environment interface. So, to keep your body temperature constant, the temperature delta needs to be your metabolic rate multiplied by the thermal resistivity.

The thermal resistivity depends on, among other things, the material you're surrounded by. That's why if you wear insulating clothes, you're comfortable at a lower environmental temperature (i.e. higher temperature delta).

To this you can add the effect of convection: if the air is moving then you don't accumulate a layer of warmer air around you, so the effective temperature delta is higher. And unless you're in a hot tub or air at 100% relative humidity, then some of the heat you produce goes into evaporating sweat. It takes energy to vaporize water, and this energy is locked into the water vapor until it condenses somewhere else.

The human body is producing about 80 watts of heat just from basic metabolism (unless you're dead) which you need to dissipate to keep your body temperature from going up. The rate of heat transfer out of your body is proportional to the temperature difference, so the environment needs to be cooler than your body.

If your environment was exactly the standard body temperature, your body would actually get hotter until the temperature delta was enough to dissipate 80 watts, which would likely be too hot to survive.

Falcon 9 was designed from the beginning with safety factors consistent with human-rating, rather than the lower safety factors required for cargo (1.4 vs 1.2 if I recall correctly). And with the very first cargo Dragon flight in 2010, SpaceX talked about how the windows and life support system pointed towards their ambition of flying humans on the spacecraft.

Now, as always happens, actually completing the human-rating of Dragon required more work than expected, and Dragon 2 is quite different from Dragon. But, as far as I know, Falcon 9 did not require nearly as many upgrades to be human-rated.

It's hard to pin it down to just a couple of things, because I came across SICP early in my programming life and it changed so much of my approach to the art. But here are a couple:

1. It taught me to think of programming languages as constructed things, rather than just being "there" and immutable. In particular, to think about the purpose of each language feature, and separating features into core primitives vs. syntactic sugar that could be reduced to those core primitives. It becomes harder to do this for "complicated" languages like C++ and Python, because many of their language features are not for one purpose but bundle together lots of disparate ideas. But it's still worth making the effort to see what choices the designers of those languages made, and how different choices would give you different points in the space of programming languages.

2. Once you have a small enough "core language", you can start thinking about algorithms that operate on programs. I had always thought of programs as expressing algorithms that operate on data, but didn't think of programs as data themselves. Of course every program is text, but in complicated languages with many constructs it seems horrendously hard to write programs that operate on other programs and change their meaning. But if your language desugars to a simple core language, the ability to transform programs opens the door to techniques like automatic differentiation of programs, probabilistic programming (like Church), and many others. These would now be called domain-specific languages, but those are often thought of as limited toys for very specific tasks. Instead, I like to think how every task has the "right" language to express it, and when you do API design you're really embedding a DSL in some "host language".

Since you asked, the other big development in my approach to programming came from learning Haskell and embracing types as an elegant way of expressing universal truths about programs. Sometimes the type of a function fully determines what the function can be, like how the only function of the type (forall a) a -> a is the identity function; this idea becomes more revelatory with more complicated types.

I don't use functional programming very much in my day-to-day life, but I think learning these ideas has shaped my approach to every language. It's not really about the superficial "functional patterns" that people often think of, like using map and filter and such, which is often idiomatically wrong in many other languages.

I think the user-friendly way to make programming less one-dimensional is what we usually do, outside of shell pipelines; give names to intermediate values:

  do x <- computation1
     y <- computation2 x
     computation3 x y

But, and perhaps this is an academic question, what if you're stuck in a context where you can only create computations by composing functions in a sequence, without giving names to intermediate results? Shell pipelines, for example, without using temporary files or other tricks.

Then, using this idea of strong and weak monads, and if you were used to thinking of computations as elements of a monad type, you might realize that all you need to add is a "strength" operator, and you would regain the full expressivity of data flow graphs. This operator would take a computation and bundle it with value, producing a new computation that does the same computation, but bundles its result with the extra value you supplied. So you've given every computation a side-channel that ferries any data you like through it, unchanged. Computations further down the chain can access both values.

I lack the imagination to see how this example works out in shell, because there we don't have the luxury of multiple input and output values (just single pipes of data). But it's nice to know that just the strength operation is enough to express arbitrary computation graphs, with names being given to inputs and outputs.

I think the article is an attempt to make your idea more precise. What if monad 3 could use the result of monad 1, not just monad 2? Then you couldn't write that computation using your pipeline metaphor.

The article is saying that by judicious use of a "strength" function, you can in fact write any monadic computation as such a pipeline (or composition of monadic functions).

I agree that it would be interesting to learn what non-strong monads look like. But the blog post does (implicitly) answer some of your questions:

It says that all monads in the Set category are strong. That would include Haskell monads, at least those expressed in the usual way as type constructors, to the extent that Haskell types model sets.

And you can see that the "strength" operation relies on the existence of tuples behaving like Cartesian products of sets. Such objects might not exist in other categories.

Yes, Starlink satellites have inter-satellite laser links that can provide connectivity even if there's no base station nearby. These have been active since November 2022 [1]. They were supposed to expand coverage to most of the Arctic in early 2023 [2], which indeed seems to have happened [3].

[1] https://www.reddit.com/r/Starlink/comments/yllqk6/space_lase... [2] https://www.highnorthnews.com/en/elon-musks-starlink-expands... [3] https://www.starlink.com/map

Negentropy? This is a concept in information theory, but maybe also in physics.