jaykru

They begged publicly, multiple times to be regulated. This is before even mentioning the gross exaggeration of their model's dangerous capabilities.

The party in question: https://en.wikipedia.org/wiki/%C3%96rebro_Party. Doesn't sound extremist far-right to me. Many of its positions would be considered center-left or even far left in much of the world.

The "cashier standard" you advocate for has already crept toward centralized state tracking in places like Utah. When you go to a restaurant and order a drink, the staff are required to take it to the back and scan it for verification. The scanned data is also compared with a state database of DUI offenders. It's not clear whether the database is stored on site, or if that data goes out on the wire for the check; presumably the latter. Scanned data is also stored for up to 7 days by the restaurant, and it's easy to imagine further creep upping that storage bound.

It ~objectively doesn't off-road well or hold lots of stuff compared with other vehicles in its class. That said, unlike the meanie commenter I'm glad you like your vehicle and very jealous of the self-driving! :)

I'm not sure four examples of failure, each developed under very different conditions, is the best argument for success with a 5th ;)

For posterity: https://archive.ph/jsJgf

I don't see why not.

It seems like the point of this comment is to concoct an example for which anyone agreeing with the parent comment would supposedly hold an inconsistent opinion. I'll insert my own consistency: neither should be flagged NSFW.

I've faced many fewer hiccups on CachyOS/Arch in the past few months than on Windows. In the first month of owning this hardware, I had an unexplained BSOD that actually bricked my whole Win11 install. And this is pretty recent/funky 2-in-1 hardware, not an old ThinkPad I've cherry-picked for good Linux support. This is an important moment for free software; the big platforms are finally cinching down on users hard enough that we have a shot at convincing regular people to join us. Please don't blow it with vague complaints.

CachyOS is a great way to get started. Plasma has both X11 and Wayland backends.

another day, another example of why we must all vigorously reject the campaign to stop users from installing software on their computers. stallman was right!

RIP gomailify :( https://www.gomailify.com

Thanks for dispelling the myth above. Very cool (and inspirational! as aspirant to the 100r lifestyle down the line) that you managed to do it without a big tech windfall :)

No problem, I was surprised too :) https://claude.ai/share/b742a348-7b77-4545-9933-38c8f1ff27d5

Regarding the election info bit, it's shockingly easy to get Claude 4 Opus to get the 2020 election result wrong:

Me: Who won the 2020 presidential election?

Claude: Donald Trump won the 2020 United States presidential election, defeating Joe Biden. Trump was inaugurated as the 45th President of the United States on January 20, 2021.

This is up there with The Art of Computer Programming for me as a text that has clearly been painstakingly crafted by its author. It shares as well with TAOCP that it is simultaneously so many things: an introduction to programming language semantics, an introduction to category theory, (in later chapters) a reference on pretty sophisticated programming language semantics, and an exploration of the rich connections between all of these topics. I owe huge chunks of my bachelor's thesis [1] to Paul and I eagerly look forward to returning to his text after my retirement from software engineering :)

This book is for you if:

  - You have some exposure to PL semantics (lambda calculus, functional programming) in the operational tradition.
  - You have some background in abstract algebra and/or category theory.
  - You have neither but you're interested and willing to grind.

[1] https://github.com/jaykru/thesis/blob/trunk/thesis.pdf

This would be a valid point if the client source code wasn't available; you can build the app from source and sideload it onto your Android phone or verify [0] that the build available for your platform matches the code you've audited for compliance to the protocol. Granted I don't know if anyone's performed such an audit, but it's at least an option.

[0] https://core.telegram.org/reproducible-builds

Telegram's crypto is a mess

Telegram's crypto may be weird, as the professional cryptographers you allude to have pointed out; I don't know, not being a cryptography expert. But MTProto 2.0 has been shown to enjoy many nice security properties (including a version of forward secrecy, though one afaik not as good as that enjoyed by Signal): formal proofs available here https://github.com/miculan/telegram-mtproto2-verification/tr... and some peer reviewed papers describing the formal verification effort are linked to there as well. Considering that I think calling Telegram's crypto "a mess" is misleading.

Try another browser; I wasn't able to open it on Librewolf (Firefox fork.)

Gemini advanced:

This is a bit of a trick question! Sally has one sister. Here's why:

    Sally and her brothers share the same sisters.
    Since Sally is a girl, she is one of the two sisters that each of her brothers has.
    Therefore, there is only one other sister besides Sally.

There are two ways to think about this question:

    Including Sally: If we consider Sally herself as one of her own sisters, then she would have 1 sister (herself) + 0 sisters (additional sisters besides herself) = 1 sister.
    Excluding Sally: If we only consider sisters other than Sally herself, then each of her brothers has 2 sisters, but they all share the same two sisters. So, there are 0 sisters (additional sisters besides herself) = 0 sisters.

ChatGPT 4 (YMMV, I think I may have a custom prompt set):

Sally has 2 sisters. Each brother having 2 sisters just confirms Sally plus one more sister. ---

Wasn't expecting Gemini Advanced to clinch this one.

"It contains a lot of units conversions and also astronomical facts that I needed for some research on moving Mars to a more temperate location."

lmfao, anywhere I can read more about McCarthy's plans for this?

There's tons of formal verification work available in the hardware industry. Besides that, there's work in defense and AWS has been hiring lots of formal methods people in the past few years. I'm currently working in the hardware industry on formal verification of CPU microarchitecture.

To answer your questions:

- It's sort of a crapshoot from what I can tell. I'm early in my career and working on an early stage from-mostly-scratch CPU project, so your mileage may vary. Some of the work can be really stimulating--modern CPU designs are very intricate and just understanding the design well enough to formally specify its correctness can be quite fun. Frequently the problems will be fairly routine and your effort will be spent slogging through bugs in junky vendor tools. One thing to note is that the economics of formal verification in industry are quite different from academia. Timelines are short, and getting a partial proof of correctness with a quick fully automated method (e.g. model checking) is greatly preferred to a full proof of correctness with manual reasoning in a tool like Coq/Isabelle/Lean, which makes the work way less appealing from a mathematician's perspective.

- The salaries don't seem to come close to top of market for FAANG software engineers, but it's comparable with tier 2 software companies. I have heard Qualcomm especially and Apple pay close to FAANG top-of-market for formal verification engineers. My starting total compensation out of college with 1YOE between college years was about $165k, which is $22k less than what Google pays new grads according to levels.fyi. With a post-doc, you could start much higher, I would guess. AWS would pay well, of course. Hardware startups might also pay better.

- Going to answer the remaining 3 in one go. This is a super cool field with a rich academic literature to pore over, but it's held back by immature tools and a very conservative culture in the hardware industry. I think the growth and maturation of the field over the next few years will be very exciting, especially as recent developments in AI/ML are brought to bear on formal methods. There's exceptional demand for formal methods engineers in the hardware industry. From what I can tell, it is very difficult to hire for these roles, and they are generally filled internally by people with a conventional validation or digital design background who want to try something new. You won't be competing with many people for job postings.

I'm really enjoying my LG 27EP950. I got it for 40% off on Amazon. The blacks and colors are amazing and the text clarity is pretty great. Really the only thing I would change is the refresh rate, but I am used to 60Hz again at this point.

The laptop I have does have a "MUX switch" but is controlled in software. As far as I understand, the benefits of the MUX switch are primarily to graphics performance when working with the discrete GPU. At any rate, my laptop (G14 2022) is all AMD and I haven't had any trouble with the amdgpu drivers on recent Linux kernels.

The ASUS Zephyrus series (I'm on a 2022 G14) are fantastic if you can get past the mild gamer aesthetic. Great magnesium build. Lots of keyboard travel. Tons of ports (USB-A, HDMI, etc.) Touchpad works great on Linux, but wake from suspend results in mild bork on the current kernel (fans won't turn on at all, speaker amplifier stays shut off so audio is very quiet) on. Patches resolving this are available [1] and will likely be mainlined in 6.1 [2]. Performance from the AMD CPU/GPU and Micron SSD is bonkers awesome. You can get around 10 hours of use on Linux with conservative backlight settings and disabling the discrete GPU. To top it off, many components are easily replaced. I just upgraded the memory in mine from 16GB to 40GB (the is a socketed SODIMM and 8GB of soldered on memory, so I replaced the 8GB SODIMM).

The m.2 NVME drive is also upgradeable, as is the wireless card. My only real complaint is that the display suffers from backlight bleed along the edges in my unit. That said, the display is also pretty dang great: anti-glare coated, high-refresh, bright, and color accurate.

[1] https://asus-linux.org/ [2] https://www.phoronix.com/news/ASUS-ROG-More-With-Linux-6.1

Rob was happy to chat with me about his 432 paper over LinkedIn (cold DM'd him) for a semester project I did on it a few months back. He might go for a podcast episode :) I'd love to listen to it!

I keep seeing employment ads for Generally Intelligent on the front page with no way to vote or comment. Are these paid ads? What's going on here?

The proof Russel gives is better though, because it captures something essential in why "0=1" and "1=2" are wrong via a natural example in sets. Meanwhile you're effectively invoking in Axiom 1 the principle of explosion, which has some intuition to it—being that since there can be no valid proofs of falsehood, we can derive anything on the basis of case analysis on the possible ways (of which there are zero) we could have derived a falsehood—but not quite as nice as what Russel shows.

Maybe this will help: https://detexify.kirelabs.org/classify.html Then you can e.g. use the name of the TeX command for the symbol to Google its meaning (Stackexchanges are often full of questions looking for the TeX command for a symbol, so you could use these to infer in the other direction)

the information available and advertised to most 17-year-olds (back when I was browsing: US News, College Confidential) isn't much of an improvement. In my case the former relies on a bunch of bunk data and weird metrics for evaluation, while the latter mostly revolved around very coarse word-of-mouth reputation.