Lightnews — Scholar-powered news

Richard Laughlin

@richardwlaughlin.com

54 followers 110 following 120 posts

Software Engineer & Researcher. Interested in automated translation of C/C++ to Rust, and taking Clang-based static analysis to a global scale 🌳✨ https://github.com/rcythr

github.com

Posts Media Videos Starter Packs

Pinned

Richard Laughlin @richardwlaughlin.com · 25d

Look Rust is great, but if they're going to accuse you of using an esoteric language anyway then you should claim as much territory as possible and write everything in LEAN.

Richard Laughlin @richardwlaughlin.com · 2d

All earnings*. There's tons of exceptions in the tax code.

Looks like there's an exception for settlements related to physical injury, but not IP theft. I kind of thought there might be one for this too 🤷

Richard Laughlin @richardwlaughlin.com · 2d

Do you have to pay taxes on it?

1 2

Richard Laughlin @richardwlaughlin.com · 2d

Follow up: Knowing that the formal guarantees are better than the current state, is it ethical to be an accelerationist and build the bots that flood the world with slop code?

Richard Laughlin @richardwlaughlin.com · 2d

Look at the bright side:

If the LLMs flood the world with slop then the only trustworthy code in open source will be code that comes with formal proof of safety guarantees.

Finally formal methods in the mainstream!

1 2

Richard Laughlin @richardwlaughlin.com · 3d

This sounds like a strictly worse version of refinement types. You can get the real thing in rust using Flux.

Though I've only used it for toy problems so far.

flux-rs.github.io/flux/

Introduction - The Flux Book

flux-rs.github.io

Richard Laughlin @richardwlaughlin.com · 4d

Unfortunately in 2025 you'll need to be more specific about which disaster

Richard Laughlin @richardwlaughlin.com · 12d

Technically it opens a local copy of the docs, so it works even better on an airplane or from a tent in the woods :)

Richard Laughlin @richardwlaughlin.com · 12d

rust-analyzer supports this and it's great!

1 1

Richard Laughlin @richardwlaughlin.com · 12d

Betteridge's Law of Headlines

QED

Richard Laughlin @richardwlaughlin.com · 13d

Space alien level of bad decision making.

Have they ever seen a visualization before?

Richard Laughlin @richardwlaughlin.com · 14d

I'm told they used to print them on ground up tree carcass. Weird

Richard Laughlin @richardwlaughlin.com · 21d

Someone in the US broke US law in sending them, but everyone else was operating legally under the law that applies to them.

By the time it got to the company who wanted to buy one it changed hands enough times that it wasn't under the table anymore.

Richard Laughlin @richardwlaughlin.com · 23d

It's ultimately the same underlying system except it uses a different window manager which feels more like windows. Ubuntu tends to feel more like a Mac.

I've found former windows users tend to feel less culture shock on Kubuntu.

Richard Laughlin @richardwlaughlin.com · 23d

I don't want to overload you with options because Linux has infinitely many, but another one you should consider is a flavor of Ubuntu called Kubuntu.

kubuntu.org

1 2

Richard Laughlin @richardwlaughlin.com · 23d

You can set up a thumb drive with Ubuntu on it and try it out before you commit. Ubuntu is probably the most user friendly distro to start with.

ubuntu.com/tutorials/tr...

Try Ubuntu before you install it | Ubuntu

Ubuntu is an open source software operating system that runs from the desktop, to the cloud, to all your internet connected things.

ubuntu.com

1 1

Richard Laughlin @richardwlaughlin.com · 23d

Yeah when I introduce TNG I always explain that the first season is rough but the rest is some of the best television ever made.

Thankfully, there's enough good content in the first season that it usually works out.

Richard Laughlin @richardwlaughlin.com · 24d

Most of these features are not meant to be used for real problems. They exist solely to be referenced on a slide for marketing and investor relations.

Richard Laughlin @richardwlaughlin.com · 24d

It'll no doubt still out live me, but then again so will FORTRAN.

Richard Laughlin @richardwlaughlin.com · 24d

It's been doomed for a while.

The unwillingness to even discuss a scheduled ABI break has caused the large scale actors to plan and start executing transition plans. Once they're gone it'll be relegated to only those unfortunate enough to be stuck.

1 1

Richard Laughlin @richardwlaughlin.com · 24d

It certainly feels awful, doesn't it?

To come all this way hoping to use a type system to obtain a cheap proof soundness, and ultimately decide for a primitive type of garbage collector because that troublesome '&' makes the interface slightly more annoying to use. 😂

Richard Laughlin @richardwlaughlin.com · 24d

Many times I wrote it the clever way that sucked to use and then I decided Arc<Mutex<InnerT>> wasn't so bad afterall.

1 5

Richard Laughlin @richardwlaughlin.com · 25d

The committee is run by compiler vendors who want to minimize support calls and do as little work as possible.

Modules solve the slow compile time complaint vendors deal with regularly, and memory safety is the user's problem.

Richard Laughlin @richardwlaughlin.com · 25d

Turns out Sean Baxter was entirely earnest, but the committee remains themselves.

1 1

Richard Laughlin @richardwlaughlin.com · 25d

There's even a section which uses absurd names solely to satisfy previous positions from the committee which lead to the absurdity of `std::unordered_map`

1 1

Richard Laughlin @richardwlaughlin.com · 25d

Yes, I agree that that's a factor.

When this proposal was first submitted I thought the author was trolling the committee with a proposal that would work, but that they knew would go nowhere for exactly this reason. Thus proving the committee is unserious.

1 1