jfmc

5 ms·

1.
by jfmc 4mo ago
!/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 infor
2.
by jfmc 10mo ago
Right!
3.
by jfmc 10mo ago
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
4.
by jfmc 10mo ago
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.
5.
by jfmc 2y ago
Other playground (wasm based): https://ciao-lang.org/playground
6.
by jfmc 2y ago
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 prov
7.
by jfmc 2y ago
Wrong capitalization makes me feel really axious and frustrated.
8.
by jfmc 2y ago
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 popul
9.
by jfmc 2y ago
A classic library, you can play with it here: https://ciao-lang.org/playground/#https://github.com/ciao-la...
10.
by jfmc 2y ago
No constraint optimization can replace Pentafunk Jenny ;)
11.
by jfmc 2y ago
Prior art: Eisenfunk - Pong ( https://www.youtube.com/watch?v=cNAdtkSjSps )
12.
by jfmc 2y ago
Xapian is used in https://www.djcbsoftware.nl/code/mu/ for indexing emails.
13.
by jfmc 2y ago
Another table (in the same thread) comparing more systems: https://swi-prolog.discourse.group/t/porting-the-swi-prolog-...
14.
by jfmc 2y ago
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.
15.
by jfmc 3y ago
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
16.
by jfmc 3y ago
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 no
17.
by jfmc 4y ago
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", whi
18.
by jfmc 4y ago
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
19.
by jfmc 4y ago
One of the co-authors here. Thank you for these helpful clarifications!
20.
by jfmc 4y ago
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'.
21.
by jfmc 4y ago
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-...
22.
by jfmc 4y ago
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 be
23.
by jfmc 4y ago
We need robopsychologists.
24.
by jfmc 4y ago
"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.)
25.
by jfmc 4y ago
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
26.
by jfmc 4y ago
I have the strange feeling that WASM is reinventing the wheel at each step and that they should have continued with PNaCL technology.
27.
by jfmc 4y ago
https://webassembly.org/roadmap/ I fear they will run out of gas before the interesting features there are completed...
28.
by jfmc 4y ago
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 drive
29.
by jfmc 4y ago
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
30.
by jfmc 4y ago
In a few years you'll be able to buy GitHub stars as NFT.

More ›