For example, you can ask whether a Java program, run with infinite memory, will eventually halt. For any particular Java program, there's obviously an algorithm that says whether it halts or not. The algorithm is a single statement, which says either "yes" or "no". Might be hard to figure out which is the correct algorithm, but the Java program is fixed so the algorithm is definitely one of the two.

However, there is no algorithm which can take an arbitrary Java program as input and determine whether it will halt. It's about the class of all possible programs.

The median of an even number of values is typically defined to be the mean of the two middle-most values.

Ah, this is what the description (what git would call the commit message) is for. You can set the description even before you've made any changes.

For example, this input:

    13- 2  *5 + 4

    "13" "-" "2" "*" "5" "+" "4"

    "13" "2" "5" "*" "-" "4" "+"

    (+ (- 13 (* 2 5)) 4)

If you want to enter the number `13`, that should be one token, but there's no way to make a `13` token in this UI. You need to stick to single digits for this site to work correctly.

    1 0 0 + 8 8 / 4

I'm completely sure that the way they worded the question the headline is about was very generously worded and that the phrasing in the headline misrepresents what it asked, because that's how these things work. Not that anyone is at fault, of course, the headline isn't a lie, and of course there are other reasons that the survey is hidden behind a subscription wall. It just so happens that the percent of people with screen-related visual discomfort according to the eye-care company survey is, I dunno, 2x higher than it would be if you asked the question directly. That's just how these things work.

(I suspect that someone is going to confuse this comment as me saying that eye-strain from screens isn't a problem for a lot of people. Pre-empting that by agreeing that, yes, of course eye-strain from screen is a problem for a lot of people.)

Still, every algorithm that's actually labeled a CRDT shares a magical property: if my replica has some changes, and your replica has some changes, our replicas can share their changes with each other and each converge closer to the final state of the document, even if other people have been editing at the same time, and different subsets of their changes have been shared with you or I. That is, you can apply peoples' changes in any order and still get the same result. I don't think it's useful to call anything without that property a CRDT.

Each data type is a `struct`. Each operation is a trait. You `impl` each trait on each struct.

This works even if you're using a library that has declared `struct A` and `struct B` and `trait F` and `trait G`, and you want to add both a `struct C` and a `trait H`, and fill out the whole 3x3 grid without modifying the library.

The library says:

    struct A { ... }
    struct B { ... }

    trait F { ... }
    impl F for A { ... }
    impl F for B { ... }

    trait G { ... }
    impl G for A { ... }
    impl G for B { ... }

    fn some_function(data: T) { ... }

    use library::{A, B, F, G};

    struct C { ... }
    impl F for C { ... }
    impl G for C { ... }

    trait H { ... }
    impl H for A { ... }
    impl H for B { ... }
    impl H for C { ... }

    fn another_function(data: T);

The definition of dictionary is just "Words about words" (source: Urban Dictionary), so I'd say that Urban Dictionary qualifies.

Something that cannot be proven within which formal system? Every true statement can be proven by some formal system. No formal system can prove all true statements.

(This is all about Godel incompleteness. Turing incomputability does apply though, see the sibling comments! It's important to keep them separate, they're saying different things.)

Yes, that's correct, it's provably impossible to construct an LLM that, if you ask it "Will this program halt? ", answers correctly for all programs. Likewise humans, under the assumption that you can accurately simulate physics with a computer. (Note that QM isn't an obstacle, as you can emulate QM just fine with a classical computer with a mere exponential slowdown.)

Someone's going to think that, since you can formally model computer programs (and thus formally model how an LLMs runs), that means that Gödel's Incompleteness Theorem applies to computer programs and to LLMs. But that's irrelevant; being model-able doesn't make something a formal system!

"Formal system" has a very technical meaning: it has a set of consistent axioms, and the ability to enumerate formal proofs using those axioms. For example, Zermelo-Fraenkel set theory is a formal system [1]. It has nine formal axioms, which you can see listed in its Wikipedia article. Utterly different kind of thing than humans or LLMs. Comparing an LLM to ZFC is like comparing a particular watermelon to the number 4.

[1] https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

Sometimes it's more swaps, and sometimes it's less. The vague pattern looks like Can't Believe Sort does slightly fewer swaps on larger lists, but that could also have been noise.

Why do you expect them to have exactly the same number of swaps?

> Bubble sort can do less than this.

Oh sorry yeah, I implemented bubble sort without any sort of early return, for a more direct comparison.

The number of comparisons is of course about twice as large, because Bubble Sort always does exactly n(n-1)/2 comparisons while Can't Believe sort always does exactly n*n comparisons.

https://play.rust-lang.org/?version=stable&mode=debug&editio...

Could you link to what you're talking about? And what's its big-O runtime?