someplaceguy

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)

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)

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

    return l[len(l) / 2]

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))

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, the theorem of infinite descent cannot be applied to this property with the set Z which the author specifically said he would use. Instead, it needs to be applied to the set Z\{0}, which you rightly pointed out (as well as the sibling poster).

Note that 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 simple proof steps to analyze what happens when either `a` or `b` are zero, which was excluded from the set. At this point you'd probably realize that yes, there is an implicit assumption that ¬(b = 0) which should be made explicit, and then you also have to account for the `a = 0` case, which should also be easy.

But still, the error 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  ∧  (...)

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

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

  ∃y ∈ Z. y |<| 0

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)

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

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?

Maybe this is what a white hole looks like...

I'm really curious about why I always hear about these horror stories in the US but I never hear about them happening in a EU country. Does anyone know why?

Is there any reason to use SML instead of OCaml in 2024?

* Many compilers and transpilers available. Don't like LunarML? Maybe try Poly/ML. Or MLton. Or MLKit. Or SML/NJ. Etc. All of the above are pretty much complete and production quality, and there are quite a few more.

* The language has a formal specification which means there's a document formally specifying what all the constructs in the language should do. In contrast, if you wanted to build your own OCaml compiler/transpiler/interpreter, you'd basically have to follow whatever the main OCaml implementation does, which changes from one version to the next, so you'd always be playing catch-up.

* The formal specification hasn't changed since 1997. This means that once written, your SML code should work the same forever. You no longer have to worry about your programs (or their dependencies) breaking when you upgrade to a new version of OCaml.

* Compared to OCaml, your single-threaded programs will usually run faster if you compile them with MLton, mostly due to whole-program optimization / monomorphization and unboxed native integers, reals and arrays.

* Some SML implementations have interesting extensions, which you can use (at the cost of being tied to that implementation). For example, MLKit supports memory regions (i.e. more efficient memory management in some cases). SML# (which is not related to .NET) supports seamless integration with SQL and other interesting features. Some implementations support multi-threading natively and/or different forms of parallelism. Most of them also support some form of FFI to interface with C or other languages.

* SML programs are easier to port to CakeML than any other language, since CakeML is mostly an SML subset. CakeML not only allows you to formally verify that your program is correct (or that it has certain desirable properties), but it also has a compiler that is formally proven to be correct, so your compiled CakeML programs are (mostly) guaranteed to be free of miscompilation bugs as well.

you can make 2 GPTs sing just as easily as you can make 100 GPTs sing.

What can you do with a billion GPTs?

The world's largest choir?