It doesn't need to be 100% correct. There's a place for fast sorting algorithms which are correct most of the time - basically anything non-critical, like sorting comments by upvotes.

According to the article, they couldn't find a case where it wasn't correct.

> There's a place for fast sorting algorithms which are correct most of the time - basically anything non-critical, like sorting comments by upvotes.

Nothing saddens me more than this trend of the modern web where everything works semi-probabilistically (even if it's likely for "good" technical reasons, such as, "we wrote our server backend in Ruby which is slow as molasses so now we need 230 CDN and 800 databases instances around the whole world and transformed our simple centralized problem into an horrendous decentralized one).

The central reason for me to use computers is that they are (or at least were) deterministic to a much higher degree that normal life, and so many things in the 10 last years becoming much more non-deterministic in particular on social websites is something that frustrates me every single day as it just makes the whole experience and process of using computers & the web very unreliable compared to what it used to be.

Jim Keller once said randomness was baked in the modern computer chip design. The execution routes were almost always different even if you ran the same deterministic code for multiple times. But in the end you got the same result almost every single time (“almost” has many 9s after the decimal point). But this layer of operations has been abstracted away from most of us. So don’t feel too sad... maybe the world has been like this for a long time

Today's perfections are yesterday's "good enoughs". Don't be sad for the trend. In 10 years, you will have new perfections to enjoy.

Like the probabilistic bank account balance. "You have between $10 and $1000 with the greatest likelihood being $537 (52% chance)."

There was this thread a while ago with HSBC switching to MongoDB... so, yeah, distinct possibility :-)

https://news.ycombinator.com/item?id=23507197

(The article was very light on details though, and it was probably just one team that consolidated to MongoDB, not the accounts itself... one hopes.)

A friend of mine went to a doctor, and after the medical lab the doctor told him you either have malaria or typhoid.

This trend seems to be everwhere

I think the good technical reasons are quite often the CAP theorem.

I know, but my argument is that a lot of time (not always, of course) the "distributed" issues could just be solved by not building a distributed system in the first place and just having more efficient tech stacks & a few big servers.

Stackoverflow was just using 4 db servers in 2016 (https://nickcraver.com/blog/2016/02/17/stack-overflow-the-ar...)

We suck really hard at proving code correct that was written explicitly with the goal in mind to be formally verified. The techniques there are still quite immature. I wonder how long it will take until we have a reasonably working pipeline of ML+formal verification. Maybe it's just easier to generate correct code from the spec than to learn it from examples and then verifying it with the specification?

"We suck really hard at proving code correct that was written explicitly with the goal in mind to be formally verified."

That is why I am not a huge fan of proving code in the first place. If you have a really complicated proof of formal correctness, then who guarantees you, there is no misstake in the proof itself? At least this is what I have seen in university, lots of complicated stuff on the whiteboard, with a result. And then someone figured out, it was wrong.

So I rather do lots of testing, for all known test cases.

Your automatic proof checker guarantees that there is no mistake in the proof. That's the easy part! The real question is who guarantees that your specification is what you actually want?

Automatic proof checkers still have bugs in them. However, one nice characteristic is that, since its algorithms are so general, i.e. about the language rather than about the problem you're solving (e.g. sorting), any bugs in the checker are either so common they hit every problem solution and are easily discovered and fixed, or so rare that it affects no real-world problem solutions.

The kernel of an automatic proof checker is much easier to test and verify than the programs you verify using a proof checker though.

+1 verification tends to be the easy part.

Sure, not all bugs are kernel bugs though.

> So I rather do lots of testing, for all known test cases.

How is this any different? You can still make mistakes in your test code, test data, omit cases that would fail, etc. I think I'd be less confident in a set of unit tests than I would with an automated proof checker.

Tests are simple to unterstand.

Complicated proofs I do not understand, without much effort.

And I surely know that you can make mistakes with test cases as well. So I surely do not claim my way to be superior. But it works way better for me.

Test cases are not necessarily simple to understand.

Especially the test cases needed to trigger some deep bug.

And so aphyr gets paid, for instance. You may not even be able realistically to run a test case. The laws of life say your 10000 core compute job will fail non-deterministically only after a day or so. It would clearly be helpful to have at least some formal guarantees, such as liveness at some level.

Well designed ML techniques are always correct 99% of the time. Its the 1% that is the problem.

99% of the time it works all of the time.

Like humans.

How do we deal with problematic humans?

Retraining or replacement.

No, we deal with 99% accuracy in humans by designing all our human-based algorithms to be resilient against mistake (and still mistakes in the end result happen very frequently). This is completely different from the way we have designed our computer systems, because it's way easier to do this with flexible agents like humans than with inflexible agents like computers.

So, the mistakes algorithms make are different to the mistakes humans make?

That’s... equivocation.

Both humans and ML algorithms are flexible. That is the point of “learning”.

Adaptation.

But the problems where we apply human labour are vastly different from the ones where we apply machine labour. In (most) tasks where we apply human labour a few errors are tolerated.

This seems irrelevant.

Neither humans nor ML make zero errors.

Ceteris paribus, if an ML algorithm makes fewer errors at a task which with low error tolerance - you would use the algorithm instead of the human, no?

I would expect that might depend on what sort of errors each make, no?

That is not practical when you expect the system to be correct 100% of the time and make decisions based on that. There are many situations where this is critical. You would never want your car's safety system to be correct only 99% of the time.

If you expect 100% correctness you are not a very practical man.

Perfect is the enemy of good enough.

And good enough is the enemy of perfection.

I suppose it depends on your end goals.

Over-achievement of my goals is not my goal.

With humans, we can ask what went wrong and fix the problem.

With black box algorithms, we throw in some new training data and just hope it's enough.

> With humans, we can ask what went wrong and just hope we've fixed the problem.

> With black box algorithms, we throw in some new training data and just hope it's enough.

A small wording change and they're equivalent again.

To some extent human beings are also a black box - with some very peculiar failure conditions and side-channel weaknesses.

No, we don't do anything against the humans who are 99% correct. 99% is good enough in most real world cases.

what's the promote option in this analogy?

ML took your job.

Call me naive but, wouldn't feeding it random input and expected output sorted by existing and proven (but slower) sorting algorithms do the trick?

For an exact proof of correctness no, because that would only show the algorithm is correct for a selected set of input-output pairs.

However, it is true that validating it for a very large number of inputs and outputs has value. This is not uncommon even in mathematics. For example, Goldbach's Conjecture (https://www.wikiwand.com/en/Goldbach%27s_conjecture) has not been proven but has been shown to hold for all integers less than 4 × 10^18

This is done! The existing correct algorithm is called the oracle and it’s used to validate the generated algorithm.

There’s some cool work on using neural program induction in compilers to try generate faster implementations based off the ‘oracle’ program that’s being compiled.

> neural program induction in compilers to try generate faster implementations

Can u provide more details?

I am familiar with garden-variety ML-optimization-of-combinatorical-space in compilers.

How would u even "measure" the expected performance unless these are gradual greedy changes