_vdpp

Being tall isn’t all it’s cracked up to be. Always hitting your head on things, and being short of breath all the time because the air is thinner up there.

I feel like the use of astronomy and cosmology to model and understand sub-microscopic processes seems a little… backwards? Frankly, I’m ignorant of both but my gut feeling tells me it’s a bit of a scientific dead end. Would love to hear why I’m wrong or if anyone else more educated than I am in this area shares the same suspicions.

2 messages producing the same digest. That’s actually a really interesting question.

Really well said. I think a big difference too is how far one takes a hobby. I can enjoy a comic book every now and then, or watch the Simpsons, or play a video game. But I’ve known people who plastered their cubicles with comic books, or displayed their massive collection of cartoon figurines. It’s when something becomes an obsession that I think it becomes infantilizing. This could go for “grown up” pursuits too. Wasting hours upon hours watching SportsCenter on ESPN doesn’t strike me as being more mature than reading comic books all day, and even someone whose whole life revolves around fishing or some other hobby might fall into that category. I think the key is to keep hobbies as hobbies and not make them your whole identity.

I enjoyed the first Saw, but to me it played out as more of a murder mystery than “torture porn” ala Hostel. It was dark in the same vein as Seven, but what made it interesting was the “whodunnit” aspect, not the horror.

A QEMU book would be _very_ welcome.

HGTV wasn’t a thing back in 1987

I really like this.

“Misinformation” is being used as a cudgel to suppress opinions or even facts that are, say - inconvenient - for someone’s narrative though.

Completely reasonable differences in opinion about the risk, origin, or proper mitigation of COVID were blasted as “misinformation” before they were eventually accepted by the wider establishment. The initial rush to completely censor such discussion early on is what caused all this free speech ruckus.

There’s always been nutty conspiracy talk, scams, hoaxes, lies, ignorance - especially on the internet - and we’ve learned to filter it out.

The “misinformation” label is going to backfire, though. Instead of ignoring it, people are going to take a closer look, because there’s probably something there that the labeler finds inconvenient. If it was simply untrue, then say so, call it “not true” or a “lie.”

Instead, “misinformation” is this kind of 1984-ish weasel word used to discredit inconvenient facts while maintaining plausible deniability when they turn out to be correct.

The “you can hose it out” meme took hold in my brain too for whatever reason. It’s the only thing I could have told you about it after “it’s boxy and probably has a Honda I-4 under the hood.”

Ada syntax takes a little while to get used to, but replace {} with begin/end and it otherwise feels like any other procedural language out there.

This is one of the better intros: http://cowlark.com/2014-04-27-ada/index.html

One of my favorite lesser-advertised features is the ability to return arbitrary-length arrays or sum types from functions without heap allocation due to the use of a secondary stack.

One of the more experienced embedded Ada devs out there wrote this: https://github.com/simonjwright/stack_usage

I’m not sure if it would meet your requirements or not.

Am I alone in wondering if quantum attacks on existing algorithms are still very hypothetical and may never come to fruition?

Ada fits the bill well here, with zero-footprint runtimes available and also a tool for statically determining the stack size at compile-time: https://www.adacore.com/gnatpro/toolsuite/gnatstack

A professor told me “The key to good design is experience. The key to experience is bad design.”

I was hoping this would be more like a car or airplane manual. “Failure to maintain adequate vitamin C levels may cause scurvy. Go to service center if this happens. Maintain blood pressure within limits (see specifications).” Etc.

I used ProtonMail a few years back, it was kind of “spartan”.

I had heard good things about Fastmail from other GMail switchers and signed up for their free trial account, and liked the experience.

The mobile app is great, they support 2FA with hardware security keys, and the price seemed reasonable.

My advice - just rip the bandaid off and do it. I had anticipated taking a whole weekend to update the email address on all my accounts, but it was a lot less painful than I had anticipated. Changing over ~50 accounts took me about 3 hours all told. Most services allowed me to change my email even if it used email as the “username.”

Using a password manager made this much easier, as I could easily keep track of which accounts I needed to update and which ones I still needed to do. I switched over to Fastmail and haven’t looked back.

This is the first time I’ve read “Zero DevOps” as a product feature, but it seems like a pretty good selling point.

Thanks for pointing out RVA22 - I wasn’t aware of the initiative but it’s a great idea. I still have reservations about the core architecture but having some standards for the rest of the ecosystem is a big win.

One more addition to my rant here - could we pick even more ridiculous, unintuitive names for package manager binaries? zypper? apt-get? yum? xbps-install? pacman at least kind of reminds you of “package manager”. This isn’t meant to dump all over the hard work that goes into all these. I suppose too that “install” is taken by a command which copies files with certain flags (anyone ever use this?).

Every one of these uses different flags too, so for someone who uses a number of different distros it’s a huge pain to remember them and switch back and forth.

FreeBSD at least uses the eminently sensible “pkg” command with flags like “search” and “add.”

Package managers are a necessary evil on systems where installing software scatters a bunch of files all over because of a dogmatic adherence to an obsolete FHS. It’s a huge burden on either the distro maintainers or the developers to produce new packages for already-written software, which often results in outdated or broken releases available in the package repos.

And now every language ecosystem has one or more package managers for development libs - pip, conda, cargo, npm, opam, dub, etc. - and then optional package managers like choco, homebrew, and probably some others I missed. It’s a huge mess. So instead we throw up our hands and just bundle everything we need in a container and duplicate the _whole distro_ because the “package” ecosystem is such a disaster.

The sane way to handle software installs and uninstalls would have been cp/rm.

It’s also worth mentioning that gcc has a command-line flag -fdump-ada-spec that will generate an Ada spec (.ads file - Ada version of a .h) from a C header for easy binding with C libraries.

VS Code: alt+arrow to move a line up/down

alt+shift+arrow to duplicate a line or block of text above or below

alt+ctrl+arrow for multi-cursor

ctrl+d for select next instance of a word

I have these baked into my muscle memory such that I had to physically type them it to remember what key combos they were! I feel completely naked without these combos in other editors.

It’s not always clear. For instance pilots can log night hours once it’s civil twilight, but there’s also nautical twilight and then astronomical twilight, all defined by the number of degrees below the horizon the sun is. What we consider “night” is pretty arbitrary.

Their mobile browser is actually very nice, I’ve used it almost exclusively for 2 years now.

This is incorrect, Ada's spec leaves open the possibility for GC, but none is mandated or even used AFAIK. The GNAT runtime is non-GC.

Ada is one. It splits the interface (specification) and implementation (body) into separate files (.ads and .adb). This is also unlike C which just does a "copy-and-paste" wherever the #include occurs.

This also makes its formal verification (SPARK dialect) nice because you can add pre and post-conditions to the interface without cluttering up the code body.

I've read very little detail about the Static Driver Verifier other than that it's supposed to use an SMT solver. I don't know if MS is using the same tool for other products in their portfolio or not. I've used it a little bit (it's a pain to set up) but have little information about exactly what it does, since it doesn't rely on any special annotations or specification language. Can you shed any light on more technical details about it?

With F*, Dafny and the Lean theorem prover, it seems like Microsoft (at least the research division) is moving in the direction of formal verification but I hear very little about it's use on their commercial products. Trade secret, perhaps?

The difference is that code with bugs can still compile, but proofs that are unsound won't check. Now granted, you can still prove the wrong thing or _not_ prove the thing that is supposed to make your system robust is taking place, so it's still very much a human endeavor with all that entails.

I think a dedicated red team going after a system for 6 months and not finding anything is a pretty good "unit test", personally. It's _evidence_ of effectiveness, not _proof_.