Not a mathematician, but AFAIK ZFC is a valid foundation. Dependent types helps a lot with bookkeeping, but cannot prove more theorems.

Lawrence Paulson is a great person to clarify those topics (Isabelle/HOL is not based on types yet it can proof most maths).

> but cannot prove more theorems

usually you're more interested in better ergonomics: can you do X with less work?

it's like picking a programming language - depending on what you're attempting, some will be more helpful.

and ZFC is a lot more low level than what day-to-day mathematics usually bothers with. So most mathematians actually work in an informally understood higher-order wrapper, hoping that what they write sufficiently explains the actual "machine code"

the idea then behind adopting alternative foundations is that these come with "batteries included" and map more directly to the domain language.

>hoping that what they write sufficiently explains the actual "machine code"

actual, having faith that what they write could compile, run, and pass tests, but never doing so.

Isabelle/HOL is still types. The underlying type theory of Isabelle/HOL is not theory of dependent types, but theory of simple types. Isabelle/ZF would be a better example as it encodes Zermelo–Fraenkel set theory.

Right!

It’s not really. It leads to paradoxes. There are alternative formulations which avoid these.

Uh? Could you write an example or two?

Not sure... Other Prologs compiled to WASM with very good performance is https://ciao-lang.org/playground/

The same toplevel runs also from 'node' as well.

Thanks. I will have a look. I would like to integrate one Prolog in exaequOS.

Other playground (wasm based): https://ciao-lang.org/playground

Actually, most of the paper seems a bit obvious from the computer science side. LLMs scale for really complex tasks, but they are neither correct nor complete. If combined with a tool that is correct (code verifiers, interactive theore provers), then we can get back a correct pipeline.

Wrong capitalization makes me feel really axious and frustrated.

Me too. At least they’re happy to capitalize “PhD”, oh wait, that somehow makes it worse.

Many times the algorithm that you are implementing requires a precise data flow that is not reversible, so using traditional arithmetic (is/2) is better for catching errors.

On the other hand CLP(FD) is not new at all (it is very popular for constraint programming).

Why would it be better for error handling? If you'll be using unidirectional flow only, then the point is moot. But using clp is arguably better IMO, allowing type and range checks while allowing relational execution.

A classic library, you can play with it here: https://ciao-lang.org/playground/#https://github.com/ciao-la...

Prior art: Eisenfunk - Pong (https://www.youtube.com/watch?v=cNAdtkSjSps)

Bit different though! In your example, the video is made from manually syncing with the song bpm, as the beep is at a constant rate. It's basically just a hand-made visualization of (every other) kick drum.

While the submission has the notes not at a basic 1/4 tempo, and is automatically "animated" based on the constrained optimization. Also leads to a much more interesting visualization :)

No constraint optimization can replace Pentafunk Jenny ;)

I love that video. Weird, but catchy.

Came here to post that. Danke!

Xapian is used in https://www.djcbsoftware.nl/code/mu/ for indexing emails.

And by Fastmail

And by Notmuch https://notmuchmail.org/

In itsel, Notmuch, a very interesting tool.-

s/itsel/itself/

Another table (in the same thread) comparing more systems: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...