Paulson is a lead developer of Isabelle , a proof assistant that is not based on dependent types.
> 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.
I think the author is confkating two different things.
There are technical problems with sticking to constructive purity when it comes to mathematics (setoid hell, avoiding excluded middle, real number formalization etc).
Then there are social aspects. The community's 'cultist' ( his words) adherence to constructive logic. Saying this is the reason rocq lost out to lean seems wrong.
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.
Paxos necessarily livelocks and still seems useful. More generically, all nonblocking algorithms which are only “obstruction-free” can livelock, but techniques like randomized backoff can make them quite reliable in practice (just like Paxos/Raft).
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).
Thanks for the recommendation. But just checking it out there,it seems to also follow a gamification model that forces you to click "commitment" buttons like you are some kind of child.
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].
> What are the differences between elisp and lisp?
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.
> At the time of publishing, the last decisive game in the World Championship was game 10 of the World Championships 2016 — 1835 days ago, or 5 years and 9 days. Is the singularity being reached, with man and machine minds melding towards inevitable monochromatic matches?
Very very unfortunate timing but still a valid question.
While all the points are valid what scares me most about Julia is what is covered under the section "The core language is unstable".
Recently I tried the latest beta version and came across an issue - I just could not add packages. (`] add JSON` or
). No matter what package I tried to add, it failed with a stacktrace pointing to libuv.
I tried downgrading to lower versions of Julia but no luck.
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.
Do you have a link to an open issue tracking this problem?
Several Julia core devs are also libuv maintainers or contributors. 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. The main libuv project has been reluctant to accept that change since it’s a quite advanced capability that Node doesn’t need.
> 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.
Thanks for the bug report (assuming that’s you that filed it). The change that broke this was made first in Julia’s libuv fork but is being upstreamed into libuv main. It simulates UNIX chmod functionality on Windows, which is (apparently) tricky to get right across all versions and all corner cases. Supporting that correctly has been an outstanding TODO in libuv for a long time — what you’re seeing is Julia driving the development of libuv and therefore hitting the bugs first.
This issue was reported seven days ago and is now slated to be fixed in the next release of all affected versions.
I don't buy the argument that not fastidiously following libuv upstream is an example of Julia not being stable. It's the opposite: that's an indicator of some measure of stability.
The situation could easily be opposite: suppose libuv does stupid things and breaks, and so if Julia tracks the daily build of libuv, it breaks.
"unstable" is not a word which means "staying on top of the development of every dependency". That could literally be a clause in a working definition of "unstable"!
If you lag behind in updating dependencies then there will be situations where you don't get some bugfix for a while
Maintaining your own fork is a good idea, because sometimes fixes are security issues from advisories. You don't necessarily want to jump to the latest and greatest libxy.so, picking up 75 other changes to fix one security item: those items are risky, because they can contain undiscovered bugs. You can carry the security patch for now and then drop it when you update.
Indeed. And in this case, the #3 contributor (and #1 in recent times, really) to Julia is also the current primary maintainer of libuv so it’s very unlikely that there would be any critical fixes that would be missed.
This particular example turns out to be a case where a feature was developed in Julia first and there’s some corner case on this poster’s Windows 10 setup that triggers a bug in the new feature.
I mean, this just looks like your run-of-the-mill bug, or? If you filter on the bug label on GitHub you will find many more. It would be interesting to try figure out what is special about your setup since no one has reported this bug since it got introduced (and it doesn't show up on any of the CI).
I was curious about that too. Many other people use Windows 10 and this is the first time this issue has come up, so there must be something else unusual going on here. If no one could install packages on Windows 10, we'd have heard about it.
I mean, that's bad and scary, but you did mention that you were using a beta version of julia. Finding this sort of thing is exactly why the beta versions exist.
If the beta was stable and ready for production, it wouldn't be called beta...
Oh, the problem is present in 1.6.2(current stable release) as well as v1.5.4(released March '21 available under old releases). I could not find any other 1.5+ version to try.
Oh I see I did misunderstand. Yes, that is unfortunate. I'd guess that since this made it into a stable release, it's likely a pretty tricky bug to encounter, since the failure is so spectacular.
I will say though that bugs appearing in stable releases of any software is a bad, but practically unavoidable thing. It sucks that this bites people, but it's not what I'd really call instability.
> 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.