!/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…
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…
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.
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,…
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…
A classic library, you can play with it here: https://ciao-lang.org/playground/#https://github.com/ciao-la...
No constraint optimization can replace Pentafunk Jenny ;)
Prior art: Eisenfunk - Pong (https://www.youtube.com/watch?v=cNAdtkSjSps)
Xapian is used in https://www.djcbsoftware.nl/code/mu/ for indexing emails.
Another table (in the same thread) comparing more systems: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...
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.
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…
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…
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…
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…
One of the co-authors here. Thank you for these helpful clarifications!
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'.
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-...
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…
We need robopsychologists.
"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.)
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…
!/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…
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…
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.
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,…
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…
A classic library, you can play with it here: https://ciao-lang.org/playground/#https://github.com/ciao-la...
No constraint optimization can replace Pentafunk Jenny ;)
Prior art: Eisenfunk - Pong (https://www.youtube.com/watch?v=cNAdtkSjSps)
Xapian is used in https://www.djcbsoftware.nl/code/mu/ for indexing emails.
Another table (in the same thread) comparing more systems: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...
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.
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…
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…
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…
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…
One of the co-authors here. Thank you for these helpful clarifications!
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'.
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-...
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…
We need robopsychologists.
"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.)
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…