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.

It is based on actors and "reference capabilities". These two blogs[1,2], could provide nice introduction.

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

Not the OP but

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

FWIW, I found Busuu great.

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

this looks neat. Thanks for sharing.

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

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

Thanks for response.

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

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.

An interesting episode. Recommended.

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

That is a non-sequitur right? Twitter , Google and Apple via their app stores, and now stripe are refusing to doing business not with a political party. They are refusing to doing business with people who have committed alleged(?) crimes.

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

Does it really matter though? Does it matter if I am above average or below average? I am as good as the last product I built, last library I wrote, the last game I played. I will have to see if I can improve and move on. Looking at one's standing on some world wide leader board is largely irrelevant outside of duolingo, imho.

> Async is not new at all

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 question posed by the headline, which I found didn't match the article very well

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.

+1 for Parsing techniques. Excellent book.

Very well put.

This matches my experience too. I regret buying them.

The series is not for those who were used to, but subsequently lost touch with, c++03 and earlier.

I found it better to learn the modern version by 'porting' earlier C++ code to use modern idioms.

Thank you. Loved it. Installed it a while and kept refreshing the tab. Great stuff. I would be happy to pay for using such an extension. Thanks.

> Without a thick atmosphere, any burgeoning life would have to deal with random bursts of energy that could cause damage to that lifes equivalent of genetic coding.

Is having a thick atmosphere a necessary condition for life?

Is it not possible for a mutation to result in a 'thick skinned' life form - one that relies on its exo-skeleton/skin to withstand the drastic changes? Or a color-changing 'plant' that evolved to do ultra-fast-photo synthesis when needed and move into a dormant mode, when not?

Such a thing would allow such plants and animals to move out of the seas and go onto dominate the land. (Assuming, of course that there is life underwater)

> They don't know the effects yet.

That's what makes it 'pseudo'.

> How is the program like 'ls' going to see a variable that is an array when originally it was a string delimited with ':'?

There are two things here: the command 'ls' that you type on your shell and the executable named 'ls' located in "/bin/ls" (or wherever) which can list directories. Most shells, when encounter a command X (say, 'ls') they see their 'context' to see if 'X' is defined. If yes, they will execute it. If not, they will assume that the X is an executable and try to execute it. That's what happening here.

Perhaps the following silly script helps?

   #!/bin/ls
   ls () {
      echo "MYLS $*"
   }
   
   ls $*

HTH

Thanks.

> I've worked a lot with LispWorks and tuning the gc had the same method of programmatically calling a full GC after every N operations.

What is "full GC", here? Do you mean, even the "older" generations? (Assuming Lispworks also has generational GC a la sbcl)

In other words, Would it have helped if the implementation was a mark-compact rather than generational?

Very informative. Thank you.

Anyone here has any experience with the GCs of Allegro or LispWorks or any other commercial Lisp implementations?

Yes. Conduits and iteratees too, for that matter. And I believe, there was some talk about "Machines", which I did not understand at all. Am not sure what is the current status of that approach.

I thought conduits and io-streams are preferred over pipes.