LessWrong 2.0 Reader

Probably it would have been worse as a perpetual draft.

I think all the assumptions that go into this model are quite questionable, but it's still an interesting thought.

I don’t know about making god software, but human software is a lot of trial and error. I have been writing code for close to 40 years. The best I can do is write automated tests to anticipate the kinds of errors I might get. My imagination just isn’t as strong as reality.

I think it is incorrect to say that testing things fully formally is the only alternative to whatever the heck we are currently doing. I mean there is property-based testing as a first step (which maybe you also refer to with automated tests but I would guess you are probably mainly talking about unit tests).

Maybe try Haskell or even better Idris? The Haskell compiler is very annoying until you realize that it loves you. Each time it annoys you with compile errors it actually says "Look I found this error here that I am very very sure you'd agree is an error, so let me not produce this machine code that would do things you don't want it to do".

It's very bad at communicating this though, so it's words of love usually are blurted out like this:

Don't bother understanding the details, they are not important.

So maybe Haskell's greatest strength, being a very "noisy" compiler, is also its downfall. Nobody likes being told that they are wrong, well at least not until you understand that your goals and the compiler's goals are actually aligned. And the compiler is just better at thinking about certain kinds of things that are harder for you to think about.

In Haskell, you don't really ever try to prove anything about your program in your program. All of this you get by just using the language normally. You can then go one step further with Agda, Idris2, or Lean, and start to prove things about your programs, which easily can get tedious.

But even then when you have dependent types you can just add a lot more information to your types, which makes the compiler able to help you better. Really we could see it as an improvement to how you can tell the compiler what you want.

But again, you what you can do in dependent type theory? NOT use dependent type theory! You can use Haskell-style code in Idris whenever that is more convenient.

And by the way, I totally agree that all of these languages I named are probably only ghostly images of what they could truly be. But I guess humanity cares more about making javascript run REALLY REALLY FAST.

And I got to be careful not to go there.

I feel you on being distracted by software bugs. I’m one of those guys that reports them, or even code change suggestions (GitHub Pull Requests).

Yeah, I also do this. My experience so far generally has been very positive. It's really cool when I make an issue with "I would think it would be nice if this program does X", and then have it do x in 1 or 2 weeks.

I don't know where to open an issue though about that I think it would be better to not build a god we don't comprehend. Maybe I haven't looked hard enough.

The Edge home page featured an online editorial that downplayed AI art because it just combines images that already exist. If you look closely enough, human artwork is also combinations of things that already existed.

One example is Blackballed Totem Drawing: Roger 'The Rajah' Brown. James Pate drew this charcoal drawing in 2016. It was the Individual Artist Winner of the Governor's Award for the Arts. At the microscopic scale, this artwork is microscopic black particles embedded in a large sheet of paper. I doubt he made the paper he drew on, and the black particles were part of Pate's drawing utensils.

Zooming out, one can see depictions of Roger Brown shooting a basketball, like one would see on TV. This collage-style artwork, as the description beside says, depicts Roger Brown's story.

These are the pieces that came together to form an award-winning piece of art. Even though most human art is combinations of things that already exist, I still value it. I am also amazed at AI's image creation capabilities.

You might also enjoy this review: https://nunosempere.com/blog/2023/04/28/expert-review-epoch-direct-approach/

From here:

Profit Participation Units (PPUs) represent a unique compensation method, distinct from traditional equity-based rewards. Unlike shares, stock options, or profit interests, PPUs don't confer ownership of the company; instead, they offer a contractual right to participate in the company's future profits.

Ah, so you have skill and a portfolio in writing. You have the cognitive infrastructure to support using the language as art. That infrastructure itself is what you should be trying to rent to tech companies -- not the art it's capable of producing.

If the art part of writing is out of reach for you right now, that's ok -- it's almost a benefit in this case, because if it's not around it can't feel left out if you turn to more pragmatic ends the skills you used to celebrate it with.

Normally I wouldn't suggest startups, because they're so risky/uncertain... but in a situation as precarious as yours, it's no worse to see who's looking for writers on a startup-flavored site like https://news.ycombinator.com/jobs.

And finally, I'm taking the titular "severe emergency" to be the whole situation, because it sounds pretty dire. If there's a specific sub-emergency that drove you to ask -- a medical bill, a car breakdown -- there may be more-specific resources that folks haven't mentioned yet. (or if you've explained that in someone else's comment thread, i apologize for asking redundantly; i've not read your replies to others)

Let xs be a finite list of natural numbers. Let xs' be the list that is xs sorted ascendingly.

I could write down in full formality, what it means for a list to be sorted, without ever talking at all about how you would go about calculating xs' given xs. That is the power I am talking about. We can say what something is, without talking about how to get it.

And yes this still applies for constructive logic, Because the property of being sorted is just the logical property of a list. It's a definition. To give a definition, I don't need to talk about what kind of algorithm would produce something that satisfies this condition. That is completely separate.

And being able to see that as separate is a really useful abstraction, because it hides away many unimportant details.

Computer Science is about how-to-do-X knowledge as SICP says. Mathe is about talking about stuff in full formal detail without talking about this how-to-do-X knowledge, which can get very complicated.

How does a modern CPU add two 64-bit floating-point numbers? It's certainly not an obvious simple way, because that would be way too slow. The CPU here illustrates the point as a sort of ultimate instantiation of implementation detail.

Yes, I totally agree. But I kind of got distracted with this post and wanted to get back to work as quickly as possible. But instead of making it a perpetual draft I pushed a bit further and got some MVP thing. I agree it's not that good, and adding concrete examples, and really making this more like a tutorial would be the first step I would take.

So I am wondering if doing something like this is still useful. Would it be worse if I had made it a perpetual draft or better?

The LessWrong Review [? · GW] runs every year to select the posts that have most stood the test of time. This post is not yet eligible for review, but will be at the end of 2025. The top fifty or so posts are featured prominently on the site throughout the year. Will this post make the top fifty?