MaxRegret
> how long a prograde burn lasts, how much fuel it consumes, how much calculated delta-v each burn imparts to a satellite
Yes, to the first two, but surprisingly not to the third. Since the maneuvers are short and much higher thrust than the average atmospheric drag, you can accurately pinpoint where those maneuvers are occurring. The energy gain can only come from the thrusters, and you can also use your atmospheric model to subtract out the (very small, comparatively) energy lost to drag. So you can actually calculate the delta-V of each maneuver quite accurately even if you don't know its exact duration or propellant consumption.
> One of the most interesting satellites in recent memory is one that was specifically designed to be long and somewhat streamlined to prolong its lifespan at very low orbital altitude
GOCE was an astounding mission! They were trying to accomplish something much harder though, mapping tiny distortions of the Earth's gravitational field, which required an ion thruster to precisely cancel out the fluctuations due to atmospheric drag and maintain an inertial trajectory. You need several orders of magnitude less precision to map the atmospheric drag itself.
I think the coolest aspect of this work is that without any involvement from SpaceX, and taking advantage of the large numbers of Starlink satellites, the researchers were able to use some nice modelling and statistics to get some very high-quality data.
[1] Yamamoto, M. Tomography of thermospheric density from Starlink Ephemeris: initial report. Earth Planets Space 78, 175 (2026). http://dx.doi.org/10.1186/s40623-026-02509-5
[2] https://www.sciencedaily.com/releases/2026/08/260812015212.h...
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.
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.
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.
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....
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.
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.
[1] https://play.google.com/store/apps/details?id=org.zotero.and... [2] https://forums.zotero.org/discussion/110371/available-for-be...
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.
[1] https://archive.org/details/microsoft-flight-simulator-v-5.0...
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.
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.
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.
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.
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.
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.
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).
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.
[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