Pinned toot

Announcement: here is something I worked on for a while - a language extending Datalog. It also does something that resembles type-checking. github.com/google/mangle

buraq boosted

'Graph Clustering with Graph Neural Networks', by Anton Tsitsulin, John Palowitch, Bryan Perozzi, Emmanuel Müller.

jmlr.org/papers/v24/20-998.htm

#cluster #clusters #graphs

buraq boosted

France has banned short-haul flights to destinations where the same journey can be made by train in under 2.5 hours. bbc.com/news/world-europe-6568

buraq boosted

Does anyone else suffer from web account fatigue? I feel like a large part of my day consists of entering passwords and all of the other stages that come with 2-factor authentication. Retail companies. Medical organizations. Streaming services. Banks and other financial institutions. Credit bureaus. Various web services.

Often these things have bugs but you need to go round the loop a few times before you're sure and give up for the day - or give up completely.

There's a combinatorial explosion too - for every service, for every platform the service appears on... . Setting up a new TV was pretty hard work and I still can't get Apple TV to work on it. (Which is OK because I also have a hardware Apple TV and a PS5 connected to the TV and I can get Apple TV on both of those). I couldn't get Disney+ to work (and as a result I got a free week's service when I complained to Disney).

And for each login there are security issues so that many passwords appear in databases of compromised - but there are only 86400 seconds in a day.

buraq boosted

No one learns as much about a subject as one who is forced to teach it. -- Peter Drucker

buraq boosted

Unapologetically boosting this because it's a nice story about a kid who fell in love with computing through @PyretLang (which runs fine on 6yo computers) and now runs his own education program. Go Isaac!

pigeonholed.co/starting-bayris

buraq boosted

a tip from a work colleague, an app that does live local-only transcription from any audio source on a linux desktop flathub.org/apps/net.sapples.L

buraq boosted

#WoLLIC2023 (Workshop on Logic, Language, Information and Computation), which I worked on the PC of, has released its list of #AcceptedPapers mathstat.dal.ca/wollic2023/acc . Conference is in #Halifax Canada in July. #logic

buraq boosted
buraq boosted

Prof. Julia Steinberger reports
that for 3 full days the EU parliament hosted thousands of scientists, activists and policy-makers charting a future beyond growth, but says every single journalist there she spoke to said, "my editor refuses to print any story critical of economic growth."
She is asking people to spread the word about this.
threadreaderapp.com/thread/165
#beyondgrowth #beyondgrowth2023

LLM craziness antidote 

This article by Jacob Browning and Yann LeCun is not new but I only came across it recently. It matches my thoughts and you may find it helpful next time someone claims "LLMs are intelligent" or something like that. AI and the Limits of Language noemamag.com/ai-and-the-limits

buraq boosted

Yet another person on Reddit surprised that Asahi Linux compiles stuff way faster than macOS.

"But macOS is so optimized for the hardware!" they all say... except Linux is already way more optimized in general than macOS is, for many workloads!

$ time tar xf linux-6.3.3.tar

macOS on APFS: 6.8 seconds
Linux on ext4: 1.0 seconds

Both on an M1 MacBook Air 13". That's how much faster Linux is at dealing with files than macOS.

The hardware drivers don't matter you're dealing with pure CPU workloads and an NVMe SSD. We already have cpufreq and share the Linux NVMe core, so there's nothing left to optimize there that is specific to this hardware. The only thing missing is deep CPU idle which will unlock boost clocks, but only for single-core workloads (multicore compiling is already at its max).

So yes, Asahi Linux is a good 6-7 times faster than macOS at some things. 🥳​

Edit: Of course I got a "but the filesystem!" so let's try btrfs, which is in line with APFS: 2.7 seconds. Still more than twice as fast.

But how about read benchmarks? With hot page cache (so FS shouldn't matter as much):

time ls -alR linux-6.3.3 > /dev/null
Linux: 0.26, macOS 1.00

Linux is 4 times faster at enumerating/stat()ing files.

time tar cf /dev/null linux-6.3.3
Linux 0.17, macOS 2.7

Oh wait, that's stupidly fast because GNU tar is smart enough to detect /dev/null and skip actually copying data. Let's try a tmpfs on Linux...

Linux 0.55, macOS 2.7

Still 5 times faster.

buraq boosted

Aw, this is too bad. Neeva is shutting down. Too many headwinds. Search engine domination continues.
neeva.com/blog/may-announcemen

buraq boosted
buraq boosted

COOL 2 -- A Generic Reasoner for Modal Fixpoint Logics

Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, Lutz Schröder
arXiv.org/abs/2305.11015 arXiv.org/pdf/2305.11015

@datalog Angle (Facebook, part of "glean") is strongly typed glean.software/docs/angle/adva ... ugh "The order of statements is important" 😅​

Show thread
buraq boosted

Genie: I’ll give you one billion dollars if you can spend 100M in a month. There are 3 rules: No gifting, no gambling, no throwing it away.

SRE: Can I use AWS?

Genie: There are 4 rules.

"Der Criti-Hype erzeugt damit – mit Harry Frankfurt gesprochen – eine gleich doppelte, sich selbst verstärkende Bullshit-Schleife." netzpolitik.org/2023/offener-b

@datalog CodeQL (an OO datalog developed by Semmle who were acquired by Github) is typed. see here: codeql.github.com/docs/ql-lang

Show thread
buraq boosted

I made a hyperbolic tiling of the "hat" tile. I tweaked some angles to the original Euclidean hat to make them fit in a hyperbolic plane. It's periodic here. It's derived from a paper model by @gerardwesty31:
twitter.com/GerardWesty31/stat

Here's another hyperbolic tiling by @zenorogue in March:
twitter.com/ZenoRogue/status/1
(I can't find the same viz on mathstodon)
I think in today's tiling, the hat looks closer to the original Euclidean hat shape.

Show older
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.