jfmc

!/0 is the cut. It prunes the search space. Useful to say "do not look at the other alternatives since I know they will fail" (when mutually exclusivity is hard) but also necessary to do negation in Prolog (when negated information cannot be easily or efficiently propagated).

is/2 is arithmetic evaluator. It runs only in one direction and it does not solve equations.

#>, #=, etc. are constraints, like (in)equalities over linear arithmetic. When constraints have the form of some known theory (like in SMT solvers), they can be solved (incrementally). That is called "constraint logic programming" (CLP). Modern Prolog systems are indeed CLP systems.

Prolog is older than CLP. CLP is older than SMT. Prolog+CLP systems are turing complete, can be used as programming languages. SMT is powerful but not a programming language.

Can "impure" features be avoided? Not in all cases. Think of them as 'unsafe' in Rust, but less dangerous.

Markus pushes for more purity in Prolog (using CLPFD), but sometimes some impurity (or imperative-like code with side-effects) is the best solution. Sometimes the pure solution is also the better. In other cases, it is not. Better compilers and static analyzers can reduce the friction between these worlds.

Take away: do pure code if you can afford it and it looks like a natural solution to your problem, use impure features later if you really need them.

Right!

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

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.

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

No constraint optimization can replace Pentafunk Jenny ;)

Note that "CheerpX enables you to run existing 32-bit x86 native binaries". For some reason support for wasm64 (in browsers) has been stagnated for years, which is a pity.