Excellent! I had been thinking of building something along the same lines when I switched from `zsh` to `fish`, as I had been missing `zsh_stats`. Now I don't have to and can focus on my other side project!
I think one thing that would definitely help the mold project is to have a clearer price and licensing model. The only thing I can find is https://opencollective.com/mold-linker.
It would be much easier to be able to go to my manager with that kind of information. Right now the conversation goes:
"Hey, this linker could save us quite a bit of time on our enormous executable."
"Okay, how much will it cost us?"
"Well, there is this site where you can donate on a regular basis."
Everyone seems to keep forgetting, there is already an option on iOS for developers not wanting to go through the App Store: web apps. I believe WASM can even be used these days. Except that Safari doesn't offer developers some privacy sensitive APIs other browsers do. The current side loading pressure has very little to do avoiding Apple's cut and everything to do with bypassing Apple's restrictions.
So I expect should Apple introduce a heavily sandboxed side-loading experience, we'd be seeing developers complain they are not adhering to the spirit or the law or lawsuit.
I don't understand why you think building alternative app stores is somehow a limiting factor. If you want to use some software, and the company wants to bypass Apple's protections, they'll just put a download link on their website. Why go through the hassle of registering with any "app store" at all?
And still folks think that if side loading is forced on Apple, that companies will not force us to start side loading their apps to escape this "apocalypse".
Fair enough, but to a database theoretician SQL means "non-recursive conjunctive queries". And I skimmed the tutorial and there is not a single example of using Logica to compute something recursively. Transitive closure is the canonical example for showing off Datalog.
It seems misleading to call this "Datalog". The GitHub repo even says "among database theoreticians Datalog and SQL are known to be equivalent", which is absolutely wrong without qualification. Some flavors of SQL will have recursive extensions so that they could be considered equivalent, but that is not true in general.
I can't find any mention of recursion on the original blog post or the GitHub page. Without recursion it isn't Datalog.
Probably fifteen years ago I discussed runtime code generation with some computer architects and they did indeed raise concerns about caching at the time. But now I am not as convinced this is as much of a worry as people seem to think. Sure if you were generating new code ever time you opened a file and did a write perhaps you would blow out the instruction cache with excessive amounts of freshly generated code. But if you waited to generate an optimized version of write until you see it is "hot spot" it seems like you would probably be okay.
I can only speculate, so maybe someone who knows better can correct me, but I would be surprised if many kernel syscall implementations would actually stay in cache after a dwq context switches. Especially with recent timing channel mitigations. But I'm just guessing.
And even if there are architectural issues, with processors seeing less benefit from Moore's Law I would expect computer architects to be looking for ways to eek out more performance such that they'd find solutions.
I don't see anywhere that mentions datalog in relationship to Stardog. I see OWL2 and SparQL, which as far as I can tell do not support recursion other than in experimental prototypes. If there is no recursion, it is just conjunctive queries and not datalog.
The LogicBlox platform is still in use and in active development at Infor. But yes, many of the principals have indeed left.
DOOP actually used LogicBlox before Souffle existed, but it is difficult to be competitive when Souffle doesn't need things like transactions, ACID, datasets larger than memory, incremental evaluation, etc.
> There does not seem to be any equivalent of the notion of soundness in the world of dynamic typing. However, we can still talk about whether a dynamic type system strictly enforces type safety.
My understanding is that there are well understood definitions of soundness for dynamically typed languages. The soundness theorem will generally be weaker ("your program will evaluate to a value or abort on a type confusion") but it is certainly possible to be sure a given dynamically typed language definition will never make mistakes like confusing an integer for a pointer. Though in the scheme of things such theorems are not much weaker than what you get for a statically typed language with exceptions ("your program will evaluate to a value with the given type or throw some exception").
It is possible I am misunderstanding something, but I am pretty sure that is not cat(1) implemented in CakeML. It is an implementation of cat(1) verified using the same HOL libraries, tactics, etc. that they used to verify the implementation of CakeML. I didn't look closely enough to see if they have gone all the way and reimplemented HOL inside of CakeML.
The key question for me is what about the project made Facebook uninterested in using the language or continuing development. On paper, Skip sounds quite compelling, so I assume there is some reason, if just politics.