someplaceguy

> “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone

Not good enough: `f(x) = []` or `f(x) = (if len(x) == 0 then [] else [x[0], x[0]]` are implementations that fulfill your specification and yet they don't always sort the input list correctly...

You can do that with the Codex CLI/TUI as well.

One of the most popular banks in Brazil doesn't have physical branches. It doesn't even have a functional website. App only.

> the DFA for an extended RE (including a lazy DFA implemented using derivatives, as here) is worst-case doubly exponential in the length of the expression

The authors seem to claim linear complexity:

> the result is RE#, the first general-purpose regex engine to support intersection and complement with linear-time guarantees, and also the overall fastest regex engine on a large set of benchmarks

> I still see AI making stupid silly mistakes.

In contrast with humans, who are famously known for never making stupid silly mistakes...

> Okay, that's not fair. There's a big advantage to having an external compressor and reference file whose bytes aren't counted, whether or not your compressor models knowledge.

The benchmark in question (Hutter prize) does count the size of the decompressor/reference file (as per the rules, the compressor is supposed to produce a self-decompressing file).

The article mentions Bellard's work but I don't see his name in the top contenders of the prize, so I'm guessing his attempt was not competitive enough if you take into account the LLM size, as per the rules.

All the more reason for asking the question?

> unless you were deliberately declaring and using near identical symbols.

Yes, that would probably be one way to do it.

> Which would violate the whole "Code is meant to be easily read by humans" thing.

I'd think someone who's deliberately and sneakily introducing a security vulnerability would want it to be undetectable, rather than easily readable.

> using the appropriate unicode characters might make it easier to read

It's probably also a great way to introduce almost undetectable security vulnerabilities by using Unicode characters that look similar to each other but in fact are different.

Recently I tried to reinstall an eSIM on my Android phone while overseas but was told by my carrier that the eSIM can only be activated while connected to antennas located in the carrier's country, i.e. it can't be activated overseas, despite my plan supporting call roaming and both countries being in the EU.

I don't know whether this is carrier-specific or the same for all carriers.

Even the EU's own official web portal [1] has a cookie pop-up that covers half the screen of my mobile phone when I visit it.

[1] https://europa.eu/

Awesome, thanks!

What I meant is, why is it significant whether the asteroid impacted in the spring or not?

> The asteroid in spring hypothesis suggests that the asteroid impact that led to the K-Pg extinction event, occurred during spring season in the Northern Hemisphere.

Why is that significant?

That's really cool! I wonder how soon I can buy one of these ESauron thingies.

> In the article n was set to 5. All of those arrays (except maybe 1) have exactly 5 elements. There is no variance

No, the code was:

    # If there are < 5 items, just return the median
    if len(l) < 5:
        return nlogn_median(l)

> and even if there was, it would be tiny, there is no point in talking about limits of 5-element sequences

So your point is: not all constants are created equal. Which circles all the way back to my original point that this argument is pretty funny :)

> The whole point of big-O notation is to abstract the algorithm out of real-world limitations so we can talk about arbitrarily large input.

Except that there is no such thing as "arbitrarily large storage", as my link in the parent comment explained: https://hbfs.wordpress.com/2009/02/10/to-boil-the-oceans/

So why would you want to talk about arbitrarily large input (where the input is an array that is stored in memory)?

As I understood, this big-O notation is intended to have some real-world usefulness, is it not? Care to elaborate what that usefulness is, exactly? Or is it just a purely fictional notion in the realm of ideas with no real-world application?

And if so, why bother studying it at all, except as a mathematical curiosity written in some mathematical pseudo-code rather than a programming or engineering challenge written in a real-world programming language?

Edit: s/pretending/intended/

> Ultimately when an algorithm has worse complexity than another it might still be faster up to a certain point.

Sure, but the author didn't argue that the simpler algorithm would be faster for 5 items, which would indeed make sense.

Instead, the author argued that it's OK to use the simpler algorithm for less than 5 items because 5 is a constant and therefore the simpler algorithm runs in constant time, hence my point that you could use the same argument to say that 2^140 (or 2^256) could just as well be used as the cut-off point and similarly argue that the simpler algorithm runs in constant time for all arrays than can be represented on a real-world computer, therefore obviating the need for the more complex algorithm (which obviously makes no sense).

I found this part of the code quite funny:

    # If there are < 5 items, just return the median
    if len(l) < 5:
        # In this case, we fall back on the first median function we wrote.
        # Since we only run this on a list of 5 or fewer items, it doesn't
        # depend on the length of the input and can be considered constant
        # time.
        return nlogn_median(l)

Hell, why not just use 2^140 instead of 5 as the cut-off point, then? This way you'd have constant time median finding for all arrays that can be represented in any real-world computer! :) [1]

[1] According to https://hbfs.wordpress.com/2009/02/10/to-boil-the-oceans/

    return l[len(l) / 2]

I'm not a Python expert, but doesn't the `/` operator return a float in Python? Why would you use a float as an array index instead of doing integer division (with `//`)?

I know this probably won't matter until you have extremely large arrays, but this is still quite a code smell.

Perhaps this could be forgiven if you're a Python novice and hadn't realized that the two different operators exist, but this is not the case here, as the article contains this even more baffling code which uses integer division in one branch but float division in the other:

    def quickselect_median(l, pivot_fn=random.choice):
        if len(l) % 2 == 1:
            return quickselect(l, len(l) // 2, pivot_fn)
        else:
            return 0.5 * (quickselect(l, len(l) / 2 - 1, pivot_fn) +
                           quickselect(l, len(l) / 2, pivot_fn))

That we're 50 comments in and nobody seems to have noticed this only serves to reinforce my existing prejudice against the average Python code quality.

I don't disagree with you. However, my point was that the parent poster's reasoning was flawed.

Stacking these services on top of each other in this way does not necessarily mean that an attacker has to compromise both services in order to compromise a host. The parent poster's flawed reasoning appeared to lead to a false sense of security as a result.

The person in question formalized the entire proof in Coq, which certifies its correctness.

To me, that makes your conjecture very unlikely to be true...

I'm sorry, I don't get it. What are you suggesting to be the motivation to remain anonymous in this case?

I would argue that technically, the proof has an error because the author says:

> Let X be the integers Z; for integers a,b, let `a ⊏ b` be `a|<|b`; and let the property Φ(a) be “a^2=2 b^2 for some integer b” (formally, `∃b ∈ Z. a^2=2 b^2`).

However, as you rightly pointed out (as well as the sibling poster), the theorem of infinite descent can only be used with this property when using the set Z\{0} rather than the set Z which the author specifically said he would use.

This has nothing to do with the rest of the proof about √2.

I do agree that even after this error is corrected, then the proof additionally needs to be fixed by adding a few more proof steps.

But still, it greatly confused me at first because it seemed like the theorem could not be applied in this case. I only realized the theorem could be used correctly in this case when the sibling poster suggested to use a different set.

The first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.

I think I'm missing something... isn't there an error in the proof when applying the theorem of the principle of infinite descent?

The theorem requires proving the following premise/antecedent (to deduce the consequent):

  ∀x ∈ X. Φ(x) ⟹ ∃y ∈ X.  y ⊏ x  ∧  (...)

... but I don't see how this can be proved when x=0. By substituting `x` for `0` (and using Z as the set X and |<| as the well-founded relation) you get:

  Φ(0) ⟹ ∃y ∈ Z. y |<| 0

Unfolding Φ:

  (∃b ∈ Z. 0^2 = 2 b^2) ⟹ ∃y ∈ Z. y |<| 0

The antecedent of this implication is true (when b = 0), so now you have to prove:

  ∃y ∈ Z. y |<| 0

However, this can't be proved because no `y` satisfies the |<| well-founded relation when applied to zero.

Therefore, this article's sentence doesn't seem to be true:

> Having satisfied the premises of the principle, we use it to deduce that no `a` satisfies the property

... which in fact cannot be true, because `a=0` does satisfy the property `∃b ∈ Z. a^2 = 2 b^2`, does it not? Consider `b=0`.

So what am I missing?

Edit: in fact, if the theorem could be applied in this case, then the conclusion of the theorem would be:

  ∀x ∈ Z. ¬(∃b ∈ Z. x^2 = 2 b^2)

Which is equivalent to:

  ∀x ∀y ∈ Z. ¬(x^2 = 2 y^2)

... which is clearly false when x=0 and y=0. So it seems like the theorem of infinite descent cannot be used to reach this conclusion. Some kind of false assumption would have to exist, but no false assumption was used to instantiate this theorem.

> The bet is that a compromise in both the service and wireguard at the same time is unlikely

An RCE in wireguard would be enough -- no need to compromise both.

> > people who value their retinas when working at 3 AM.

> You just need a well lit room to use light mode.

Who wants a well-lit room at 3 AM?