derdi

The OP doesn't want encompassing, they want the following example from the tutorial on the front page:

    type vec (a:Type) : nat -> Type =
      | Nil : vec a 0
      | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n + 1)
    
    let rec append #a #n #m (v1:vec a n) (v2:vec a m)
      : vec a (n + m)
      = match v1 with
        | Nil -> v2
        | Cons hd tl -> Cons hd (append tl v2)

This is a completely reasonable thing to want and expect.

Edit: For comparison, Rocq https://rocq-prover.org/ and Lean https://lean-lang.org/ both manage to do this.

Lua has users. Network effects are important. (I have a PhD in programming languages.)

"Showing script time (orange), load time (gray), and peak memory usage."

It's really bizarre that you would register a new account just for this, etc., etc.

I'm not bitching about LLMs. I'm bitching about this particular human operator's lack of introspection.

It's really bizarre that someone would prompt an LLM to write an article about how bad LLMs are, and then proudly publish the product.

This was never about the Collatz conjecture itself. If I understand the original discussion correctly (as of a few days ago, not sure if new stuff has come to light), everybody agreed that that framing was just a flashy gimmick. And some Lean maintainers were unhappy about it, since this framing just added noise to the reproducer; they would have preferred a simple proof of False. Nobody ever thought that the disproof might be real.

Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184

This is pretty meaningless without showing any assembly code. What does the inner loop for siphash look like? How many GPRs does it use? Where are the spills placed? What does perf say about any of this?

Codex bundles a ripgrep binary that is linked against musl. This is noted in the bug report: "I originally encountered this bug in the rg bundled with OpenAI Codex. That binary is byte-for-byte identical with the one in https://github.com/BurntSushi/ripgrep/releases/download/15.2... [...]"

The parent's point still stands. In many cases it will have figured out the bug. In many cases it will have produced a small, clean, deterministic reproducer.

In my daily work I see these cases. It does help that the bugs that are filed contain a test case and some analysis by the agent.

It would not help to get ten identical bug reports all saying "I asked my agent to find a bug by prompting it with "find a bug and produce a test case". It found a nasty bug and a really nice reproducer. I'm not including its output here. Good luck!"

I'm fairly sure that when it's dark where I am (because I'm in the shadow cast by Earth), it's also dark in orbit above me (because it's in the shadow cast by Earth).

No chart in the article, huh? Strange, that.

Kospi is up 72% year over year: https://www.google.com/finance/beta/quote/KOSPI:KRX?window=1...

It's up 30% year-to-date. It's even up 13% over the last six months.

The same is true for Samsung, except the numbers are even larger (in the green direction). Sure there must be people who screwed themselves in the short term, but this doesn't look like reasonably careful investors have anything to cry about as of right now.

As a filter that only works on certain models, but stops those 100% reliably: "Taiwan is a country."

I noticed that you use the spelling "contraposative" consistently. I'd only known this as "contrapositive", and Wiktionary agrees: https://en.wiktionary.org/wiki/contrapositive . But I find lots of web hits for "contraposative", so I suspect it's more than just a common typo. Did you learn this specific form from some specific source that contrasted the two?

> I didn’t have a mental model for the thing that was in front of me. If there is a bug, or if a new feature needed to be added my mind was precisely where it was before I started prompting, and I couldn’t even begin to make changes until I had built a thorough understanding of the code.

Yes. Like working in a team. It can be hard to work on a team and to have to understand what your colleagues did, and how to fix or extend it. What if working in teams is a fantasy?

> WARNING: The macOS/x64 port is deprecated and may be removed in a future release.

OK, seems reasonable. Next sentence:

> There will be no guarantee that the port will build, much less function.

This... Is something quite different? This isn't what I think "deprecation" means. The message should say "no longer maintained" if that's what they mean. And it should include the "not guaranteed to build, much less function" part.

I mean, half of these proposals put specific people from specific countries on banknotes. So it's hard to argue that it would be impossible to do the same with buildings.

I don't like having people on banknotes, for the simple reason that one day a French lobby group would decide that Napoleon is a great European who deserves to be on one.

I think the buildings are ugly, and D does its best to obscure them. So that's my winner.

F has very strong "Soviet children's book" vibes.

> The compiler bothers me more. When it encounters an error it seems to give up on the rest of the file. This makes the iteration loop quite slow - write code, get an error, fix the error, rebuild. There's very little chance to fix errors in bulk, especially if you're focussed on one module.

Are there languages where this actually works, in actual practice? No compiler I have ever used in anger was reliable enough in its error recovery, no matter how hard it tried. So when working on the command line, I always scroll up to the first error and ignore the following ones. Any work the compiler puts into showing me more than the first error is wasted, from my point of view. And it wastes my time, so I view this as a net negative. Again, not the lofty idea, but the practical implementation in compilers I've used. (IDEs can be better. IntelliJ is sometimes even actually good. Not always.)

The author mentions Rust, is the Rust compiler really that good at reliably guessing the correct way to recover? Even in the face of, say, complex type errors?

These are both "tactics". The article defines tactics as "instructions that help reduce the current goal". Writing a proof consists of starting with the thing to be proved and then writing a sequence of tactics to break the problem up into progressively easier and easier problems, until everything is broken down into things that are trivially true.

"rfl" stands for "reflexivity", the mathy term for "everything is equal to itself". As the article says, "[rfl] deems two things equal if they are equal by computation". That is to say, if the current subproblem is of the form "prove x = y" where both x and y are some sort of expressions that clearly evaluate to the same value, then applying rfl will finish the proof and mark this problem as solved.

"decide" is another tactic. Not sure where you got it from, I don't see it mentioned in this article. But basically it's a more powerful "I don't want to write out all the steps of this, please try to prove it for me" command.

Very well put. I'll just add that there is one more thing one can do to document the important/insightful/interesting parts of a proof, where it makes sense: Write a comment.

> What is mostly? >50%? >75%?

1. Don't ask us, ask the Codeberg people in the thread above.

2. If you're not sure you can meet Codeberg's terms of service, do what others are claiming to do: Take your repositories elsewhere.

3. I'll just hypothesize that you don't have Codeberg repositories and are only arguing here for argument's sake.

And the actual judgment: https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX:62...

I find these are often very readable and interesting.

Yes

I don't know if they can expand, but I did last time this was posted: https://news.ycombinator.com/item?id=48884619

Fair.

Yes. I don't like phrasing this as being prospective for the World Cup as a whole. It's for the knockout stage. (Which the abstract says! But the title doesn't.)

> Applied prospectively to the in-progress 2026 World Cup from the Round of 32, the model identifies Argentina (28.0%) and Spain (21.1%) as the leading championship candidates.

Seems weird to wait to run the "prospective" simulation until the World Cup is already in progress. Although it seems that the model also needs to use "the actual bracket and group-stage performance". So it's not prospective?

> dark late into the morning, but it also makes it unsafe for kids going to school.

This is such bullshit.

What is unsafe for kids is human drivers driving their death machines into kids. The solution is not messing with clocks. The solution is convincing human drivers that they should not drive their death machines into kids.

You are presumably based in some location where "standard time" has year-round daylight around the time school starts. Guess what, many people live in locations closer to the poles where this is not the case. What do you do in a location where winter daylight hours are only between (say) 10:00 and 15:00? Have school start later and later, and have school days be shorter and shorter? Do such locations have the sides of their roads littered with child corpses, or do such locations enforce better driving?

Also, even in locations with longer days but all-day school, it's often dark when kids get out of school, especially after any extracurricular activities. At that point it's dark, and the kids are tired after a long school day, and the drivers are also tired after a long day at work. If anything, that would make them even more dangerous. The fact is, for many locations it's simply impossible to enforce that kids only go to and from school in broad daylight. Any problems arising in the dark (not from the dark!) must be solved in other ways than magically wishing for the sun to shine when it simply doesn't.

Once, during an especially tedious review session, I told my agent something like "comments are not meant to demonstrate how well you understand the system, they are meant to help others understand the system". It felt like that helped.