amw-zero

Your whole system is a queue. Requests come in, are processed, and some output is given.

Algorithmic complexity affects the processing time of each request / task. Knowing the latency distribution is crucial in understanding the queueing characteristics of the system, and the algorithmic complexity will greatly affect that distribution.

A queue is:

* An arrival rate of requests * A processing time for each request * A corresponding queue length when a new request comes in before the current one is done being processed.

So anything that affects processing time affects queueing. Cache hit rates, data packing, etc., all affect processing time, but processing time is in the context of a queue.

Loved this writeup, because queues are the most important and general concept in reasoning about performance. When you realize this, you start seeing them everywhere. Locks, async IO... everything is just interacting queues.

Yes, but I think it's a revelation to many people that things like this map to queueing. Literally _everything_ related to performance is queueing, but we use different words for different scenarios, like "contention."

It's the most "enjoyable" language to write in my opinion. I totally agree. I wish I got to use it more at work, now it's all Go and Python.

This is an opportunity to learn. The way WebAssembly is defined is the standard way PL semantics are defined.

I think it's much better to just learn how to read inference rules. They're actually quite simple, and are used ubiquitously to define PL semantics definitions.

Constraining this on "that's not an option" is a big waste of time - learning this will open up all of the literature written on the subject.

> Users care quite a lot when these things break.

Users care when their expected behavior breaks. They certainly do not care why it broke, or _where_ it broke. Most users don't know what a database is.

> If I go down my recent list of bugs and categorize them, ~8 out of 10 of them are in areas which the author would have abstracted away.

Even though the model is abstract, all of the behavior of the implementation is covered in a model-based test. For example, let's say a SQL query is what's broken for some use case. This query would be exercised in the test, and it wouldn't pass until the query is fixed. That's the main reason I prefer model-based integration tests - there are no such bugs that escape.

Also, I still write targeted tests. There's nothing that prevents you from doing that, and it absolutely is useful in many cases. I just believe that most tests should be generated, and hand-written tests should be the minority.

For "business applications," I much prefer the variant of property testing called model-based testing. This is where your property is "does the implementation behave like some simplified model." This is the correct way to test such applications in my opinion, because users don't care about "custom widgets," "queues," or "databases." They care about business functionality, which is quite easily expressible in model form.

I don't do much mocking either, because I also prefer integration tests for these types of applications. Here is an example that tests against a database, all the way up to the state management layer of the UI: https://concerningquality.com/model-based-testing/.

In fairness, people don't write about doing this a lot. PBT literature seems to revolve around sorting functions or binary tree operations. But PBT much more powerful than just that.

We might not have exhausted their applications, but everything I’ve witnessed them being used for has been extremely disappointing.

That is, other than me using them to bounce ideas off of and create small snippets of code.

There’s a few different perspectives on this. One is, there isn’t much of a need to verify the implementation once you’ve verified an abstract specification. The costliest errors are _design_ mistakes, i.e. high-level errors that could never lead to a satisfactory implementation. Once you figure those issues out, it’s simple to write an implementation that conforms to the spec.

I think there’s actually merit to that perspective if you think about it for a while. However, I have also seen relatively simple behavior be implemented in complex ways, usually due to performance optimizations. In those cases, it’s nontrivial to know if it’s implementing the spec. But the spec can be used to generate test cases in many ways, e.g. http://www.vldb.org/pvldb/vol13/p1346-davis.pdf.

Frankly, I’ve had the most success by not using TLA+ and by instead writing executable models. And then using the model to show the expected values for interesting test cases, and then manually write test cases using those expected values.

Quint looks like _exactly_ what I’ve been looking for. It’s all the good parts of TLA+, but with sensible types, and a focus on executability.

I understand that executability makes the language much less _powerful_ in a mathematical sense. But it’s such a benefit in all other ways that I think we should focus on the specification that we can write that are also executable.

I thought they meant that it just wasn’t enough money. Of course there are more important factors to a job than just compensation.

And why is that?

That’s not a hot take. Literally thousands of people have written and said this exact same thing, for years.

Levels.fyi puts L6 at Amazon at over $400k. That’s not worth it?

There’s nothing unique about go-jet. Jooq does the same thing for example.

How does this make money? It says it’s free, and I don’t see any ads.

Try making comments that are relevant to the article.

What I’ve never understood about this approach is that it claims to be “network transparent,” but you need to add client and server annotations. So it’s very much network-aware.

LLMs are really, really bad at proofs so far in my experience. Especially proofs in proof assistant since those are machine checked and unable to be faked.

I also don't understand the obsession

What a weird thing to care about

Laughably bad advice.

What's the failure rate of startups - 90%? This is less risky than a slightly crowded job market where there's still millions of jobs?

That’s what I’m asking - did the comment mean that the async/await pattern is bad, or that asynchronous programming in general is bad?

What does this even mean, how can you do any form of modern computation without async?

Code written in F* is running in Firefox, Linux, Windows, and Azure: https://project-everest.github.io/.

This doesn't feel in contrast to what I was saying. You can reason about imperative code, but you have to add things to it to reason about it, most importantly the notion of a memory store. This is because imperative code assumes an underlying CPU + RAM which holds state.

It's not that it's easier, it's that imperative code has implicit state.

I've come to the conclusion that executability and reasoning are separate axes. If we view everything in terms of languages with interpreters, of course functional semantics must be executed by imperative machines. But to reason about either kind of program, we need functional semantics, because functional programming is the language of pure reasoning.

More on the subject: https://concerningquality.com/quality-and-paradigm/

This is precisely why humans will always be involved with creating software.