BlanketLogic

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.

FWIW, I found Busuu great.

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

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

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.

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.