Viewing profile — 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…

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 clarif…

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 t…

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…

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…

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 …

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 tha…

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 program…

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 embeddin…

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, perfor…