HNHacker News
TopNewBestAskShowJobs

jfmc

238 karma · joined April 14, 2020

submissionscomments
jfmc··on Prolog Coding Horror
!/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.

jfmc··on A new bridge links the math of infinity to computer science
Right!
jfmc··on A new bridge links the math of infinity to computer science
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).

jfmc··on Learn Prolog Now (2006)
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.

jfmc··on The Simplicity of Prolog
Other playground (wasm based): https://ciao-lang.org/playground
jfmc··on Machine-Assisted Proof [pdf]
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.
jfmc··on I sensed anxiety and frustration at NeurIPS 24
Wrong capitalization makes me feel really axious and frustrated.
jfmc··on I'm not mutable, I'm partially instantiated
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).

jfmc··on I'm not mutable, I'm partially instantiated
A classic library, you can play with it here: https://ciao-lang.org/playground/#https://github.com/ciao-la...
jfmc··on Synchronizing Pong to music with constrained optimization
No constraint optimization can replace Pentafunk Jenny ;)
jfmc··on Synchronizing Pong to music with constrained optimization
Prior art: Eisenfunk - Pong (https://www.youtube.com/watch?v=cNAdtkSjSps)
jfmc··on Xapian: Open source search engine library
Xapian is used in https://www.djcbsoftware.nl/code/mu/ for indexing emails.
jfmc··on Ask HN: What's Prolog like in 2024?
Another table (in the same thread) comparing more systems: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...
jfmc··on WebVM is a server-less virtual Linux environment running client-side
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.
jfmc··on GPU accelerated SMT constraint solving (2021)
They should compare with other multithreading and GPU approaches for SAT/SMT solving (like https://www.win.tue.nl/~awijs/articles/parafrost_gpu.pdf from Armin Biere, or other works from Mate Soos). There has been a lot of research in this direction.

Other old HN thread (2017) with relevant comments https://news.ycombinator.com/item?id=13667380 from actual experts.

jfmc··on The Birth and Death of JavaScript [video] (2014)
WASM is an extremely useful compilation target because of its portability (specially for running on browsers), but it is far from being the "default compilation target" for almost any language. The promised near-native speed is not here (in general you get x2 or x3 slower code but it can be even worse), it is limited to 32-bits (MEMORY64 is on the way but there is not a clear roadmap of when this will be generally available in browsers), blocking IO is a pain, and its design seems to be constrained by the underlying JS JIT (it still looks like ASM.JS with a different syntax).

I still believe that it is a miracle that we have WASM as a standard, and that it runs smoothly across different browser vendors, but why nobody seems to be worried about lack of progress in performance?

LLVM IR would be a much better binary target. It was used in the abandoned PNaCL project. AFAIK Apple uses it (bitcode) to store apps that are later compiled for specific platforms. WASM looks like a toy compared with this technology.

jfmc··on Show HN: Phind.com – Generative AI search engine for developers
Surprisingly it can generate Coq proofs. Unsurprisingly the "proofs" are just hallucinations that look right but make no sense at all. See for example: "coq program that proves that p->q is equivalent to q->p", which produces:

Theorem equiv_pq_qp : forall (p q : Prop), (p -> q) <-> (q -> p). Proof. intros p q. split. - intros p_imp_q q_imp_p. apply q_imp_p. apply p_imp_q. assumption. - intros q_imp_p p_imp_q. apply p_imp_q. apply q_imp_p. assumption. Qed.

... together with a lengthy and convincing explanation in natural language.

Sophists would be delighted by these mechanized post-truth AI systems.

jfmc··on Welcome to Comprehensive Rust
My impression when working with people using Simulink is that 'safety' is much weaker that for people working on formal methods, and certification limited a lot the kind of programs that they would write. It made totally sense for their domain, but -- as a general practice to write software -- it didn't impress me at all. I may be wrong.
jfmc··on The Ciao System
One of the co-authors here. Thank you for these helpful clarifications!
jfmc··on Why do arrays start at 0?
The general term of arithmetic and geometric sequences seem simpler when indexing from 0 rather than 1. I do not think that '1' is more human focused for anything than '0'.
jfmc··on Vector graphics on GPU
Didn't Chrome (and probably others) added GPU accelerated CSS and SVG (i.e., vector graphics) 10 years ago? https://www.tomshardware.com/news/google-chrome-browser-gpu-...
jfmc··on Trealla – A compact, efficient Prolog interpreter written in plain-old C
I really recognize the value of new implementations and the fact that each of them is filling a hole that old implementations do not cover (like new platform support, more embeddings, etc.).

But I have a controversial question: why is it better to start a system from scratch than contributing and helping to other less known, long running systems (Yap, XSB, ECLiPSe, Ciao, gprolog, B-Prolog, etc.)?

In the old times, a system became popular because you read a research paper which described carefully the implementation decisions and did good performance evaluations. Papers were reviewed and trusted, you could get objective information about why the implementation was good or not. This helped advance the state of the art.

Nowadays, this is completely broken and it is strangely feeling like a "popularity" contest and a social game. For example, some users were surprised about the performance of WASM-compiled Ciao Playground:

  https://ciao-lang.org/playground/
that despite being x2 slower than native, is faster than other popular Prolog implementations. We needed to tweet about it and use the forum of another popular Prolog system to have any visibility. Despite that, this fact will soon be ignored and buried.

When looking at the VM of each of the systems, we know why this happens, but the expertise of the people who wrote earlier Prolog systems, many of them run perfectly fine and blazingly fast in modern machines, is being lost.

Of course, we learned a long time ago that the selection of benchmarks is really complex. You can pick whatever is needed to make your system shine. Ciao Prolog is extremely fast for some benchmarks but it can also be much slower in others.

My claim is that despite it is cool to have new and nice Prolog implementations, this is adding a lot of noise and we are repeating mistakes from the past and going in the wrong direction:

- There is no incentive for proper benchmarking (e.g., should I implement mmap-based file mapping? when does it help? is it a good idea?) - The literature is being ignored (e.g., who reads and compares with Paul Tarau or Bart Demoen implementation papers?) - VM and libraries should be independent (it should be possible to implement a new VM while not requiring to reimplementing the whole set of libraries) - Systems copy/reimplement features without proper recognition of the original system (e.g., once a technique is adopted by the popular system, the original is forgotten, who knows that JITI was originally developed by Vitor Santos Costa in YAP?). - The community is extremely fragmented.

I wonder if it would be possible to create a more healthy Prolog forum which prioritizes ideas, authors, and results. Going through twitter, discourse, github discussions, github issues, of each of our individual Prolog system is NOT a solution. Each of us looking at decades of research papers and reproducing them in each of our systems is also not a good idea (indeed the unique advantage of old systems is that it takes decades to incorporate some of these ideas). Moreover, there are still many unsolved problems in modern Prolog systems that can only be addressed as programming language research.

jfmc··on OPT: Open Pre-trained Transformer Language Models
We need robopsychologists.
jfmc··on Ruby YJIT Ported to Rust
"YJIT code ported from C99 to Rust" Beyond passing the test suite, are there more numbers to compare both versions? (e.g., compilation time, lines of code, size of binaries, performance, etc.)
jfmc··on WebAssembly 2.0 First Working Draft
Perhaps... but 5 years without progress in some areas is an eternity. Rust in Firefox was super interesting and they run out of funding. It is really hard to explain to a client: "your application would work on WASM, on a browser, with no installation, but it will not scale in time and memory, and there is not a clear roadmap of then things will improve (despite OS and compiler guys know how to fix those things)".
jfmc··on WebAssembly 2.0 First Working Draft
I have the strange feeling that WASM is reinventing the wheel at each step and that they should have continued with PNaCL technology.
jfmc··on WebAssembly 2.0 First Working Draft
https://webassembly.org/roadmap/

I fear they will run out of gas before the interesting features there are completed...

jfmc··on WebAssembly 2.0 First Working Draft
The requirement for structured programs dates back from the asm.js hack. Both relooper and stackifier are still workarounds. CPUs do not require structure programs at all. Unless there is a really good reason this still looks a hack driven by limitations of the underlying code generation. I understand that some compilation passes are easier/cheaper with structured control. But then... why are not LLVM and GCC enforcing them as well (at least their roadmaps)?
jfmc··on WebAssembly 2.0 First Working Draft
What about pointer size? Is still only 32-bits? It is impossible to write some C programs when you do not know the size of your data and pointers.

I'm asking that because despite all the hype, wasm binaries are still 32-bit (at least in browsers), while 32-bit OS are being deprecated. 64-bit pointers are really good for some applications, with no performance degradation at all.

Does Wasm 2.0 support branch instructions needed for irreducible control flows? (without the relooper hack)

jfmc··on We lost 54k GitHub stars
In a few years you'll be able to buy GitHub stars as NFT.
Page 1 of 2Next →