> Is this the mathematician's variant of "my language is better than your language",

Almost. A closer analogy is comparing paradigms, say OOP vs functional programming.

Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof. Isabelle works differently. Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.

Firstly, there is value of the attempt. By staying true to constructive logic, there was a lot of progress (compcert verified c compiler, cubical agda etc).

Secondly, there were other confounding variables (tooling, network effects). Claiming rocq lost out to lean due to community's obsession is a bit of reductive argument.

But author is an expert. I will defer to him. His point about sledgehammer approach working well in the new AI world is very interesting though.

1. https://blog.jtfmumm.com//2016/03/06/safely-sharing-data-pon... 2. https://bluishcoder.co.nz/2017/07/31/reference_capabilities_...

USAMO : USA Math Olympiad. Referred here https://arxiv.org/pdf/2503.21934v1

IMO : International Math Olympiad

SOTA : State of the Art

OP is probably referring to this referred to this paper here https://arxiv.org/pdf/2503.21934v1. The paper explains out how a rigorous testing revealed abysmal performance of LLMs (results that are at odds with how they are hyped about).

After a year on busuu and 1000 days on duolingo, I find the former way better for language acquisition.

Comments URL: https://news.ycombinator.com/item?id=37379931

Points: 4

# Comments: 0

Comments URL: https://news.ycombinator.com/item?id=30817925

Points: 10

# Comments: 2

Comments URL: https://news.ycombinator.com/item?id=30683964

Points: 3

# Comments: 0

I published one too[0] which is much clumsier - it needs to be interacted via wordlers. Of course mine is more for trying out an algorithm or two for solving. But it also allows one to play cows and bulls[1].

[0] https://crates.io/crates/wordlers [1] https://en.wikipedia.org/wiki/Bulls_and_Cows

common lisp is a general purpose programming language with a well specified language and standard library. Elisp is intricately tied to emacs.

Notable differences are , till recently(?), elisp has only dynamic scoping for variables. Common lisp has, by default, lexical scoping for variables (while also allowing dynamic scoping). Common lisp has much better support for closures than elisp. Common lisp has very mature commercial and open source compilers that produce very efficient code.

Very very unfortunate timing but still a valid question.

> Do you have a link to an open issue tracking this problem?

Yes [#41642](https://github.com/JuliaLang/julia/issues/41642)

> The main reason for the divergence is that Julia’s libuv fork has a significantly more flexible event loop model that allows using libuv from multiple threads efficiently.

Glad to hear this. That's impressive.

Turns out it is a regression introduced by a commit dated Sep 23 2020. In libuv.

As I tried to fix it, I realized Julia uses a version of libuv that is significantly diverged from libuv main branch ("123 commits ahead, 144 commits behind libuv:v1.x" as I write this comment) and the bug was in the code. Using the code from the corresponding function from libuv upstream fixed the problem.

To summarize

1. There's a bug introduced close to a year ago that breaks basic functionality on a mainstream operating system. 2. Julia has its own version of, of all things, libuv, that is significantly diverged from the original. 3. The bug is in one of the changes introduced.

While each of the above is defensible on its own. Taken together, they do scare me away from considering Julia for production use. I am hoping am wrong somewhere. I think it is a lovely language.

One of the presenters is a novice with c++ background and the rest all are experts in their respective array programming languages.

The _actions_ by a group of people are resulting in these bans. Not the group's affiliation. Am I missing something here?

Comments URL: https://news.ycombinator.com/item?id=25508394

Points: 205

# Comments: 139

I believe GP is referring to async streams[0]. Notwithstanding the colourful language GP used, I think the new async streams are pretty cool.

[0] https://docs.microsoft.com/en-us/dotnet/csharp/tutorials/gen...

The later paragraphs do show the link between headline and the content. No? Looks like the final straw that broke him was Lloyd's infringment lawsuite accusing him of stealing from a film which he co-wrote.