The Unclear Impact

Kristóf Marussy ferdium🎀 |

I'm a PhD candidate working on the extra-functional requirements and formal verification of cyber-physical system architectures.
I also like free (as in liberty) software, privacy enhancing technologies, and cryptography.

I may not be trans but transgender hating script kiddies are too incompetent to tell the difference. Donkey Kong says trans rights = human rights.


why are our students complaining about the assignment not working out of the box instead of just… doing the assignment?

if the starter project was doing everything we requested out of the box, it wouldn’t have been the starter, it would have been the solution blobfoxconfused

type theory turned dark, coming up with weird math terminology, kinship terms

was playing around with some #StaticAnalysis for #ObjectOriented things blobfoxscience a somewhat challenging technical detail is that we can’t fully use recursive datalog queries to drive the analysis, because we sometimes have to take greatest fixed points instead of least fixed points. so we need clever ways to break the recursive knot in some places (and only tie it if an lfp sufficies)

by abuse of terminology, for a given type A, and ommer is a type B which is the direct subtype of a direct or indirect supertype of A, but is not itself a (direct or indirect) supertype of A. we call a direct subtype C of A a good child for the ommer B if squick it is a subtype of B or has a common (direct or indirect) subtype with it. we call ommers B with no corresponding good child are evil blobfoxrage

(this ended up completely backwards, because evil ommers can be handled without breaking the recursive knot, and good children gave us considerable problems)

android, development

it takes making my internal DNS resolve the development domain to and

-A OUTPUT -d -j DNAT --to-destination

but I can finally debug websites with TLS (to force a secure context) in the #android #emulator.

why can’t it just have normal bridged networking, like the rest of the VMs I run? blobfoxangry

and why does it fail to enable host GPU acceleration if I try to run the emulator from the command line (instead of android studio) to add -writable-system so I can add the internal domain to /etc/hosts? blobfoxconfused i guess it doesn’t like #swayvm much


the language where a dependency can transitively affect the types of completely unrelated global symbols:

I've been using in my recent papers. I think it really adds to the readability and understanding of the math.

Here are some examples. It uses in .

Let me know if you like it. Happy for any feedback.

An annotated equation in Latex. 

The equation: Pro[X(.) \in S] <= e^epsilon . Pr[X(.) \in S]

The first X(.) is in a red box and a red arrow points to it with the annotation, "system state" on top of the arrow.

The first S is in a blue box and a blue arrow points to it (from below) with the annotation, "S \subset Range (X)" on the arrow. Another annotated equation:

Pr[R(Tau_i, j) \in S] <= e^epsilon . Pr[R(Tau'_j, j') \in S]

Both Tau's are in red boxes and have a (bidirectional) red arrow pointing to each other and the annotation "Tau_i, Tau'_i \in Gamma, the set of Tasks" on top of the arrow.

Both j's are in blue boxes and have a blue bidirectional arrow pointing to each other (below the equation) with the annotation "j, j' \in N" under the arrow. An annotated equation surrounded by text. The equation:
Lap(x | mu, b) = (1/2b)exp(-|x-mu|/b)

The first "mu" is in a red box and a red arrow points to it from the top with the annotation, "location parameter, mean" on top of the arrow.

the first "b" is in a blue box with a blue arrow pointing to it from below with the annotation, "b>0, scale parameter" on the arrow.

We see an equation number (3) to the right of the equation. Two annotated equations side by side. 

Left equation: N_i = Q_p(t_{j+1} - t_j | for all j)

Q_p and for all j are in red boxes. t_{j+1} is in a blue box and t_j is in a brown box.

There is a long, red curly brace (sideways, pointing down) on top of the entire RHS of the equation with the annotation, "some annotation about the entire equation here". A blue arrow points to "t_{j+1}" from below with the annotation, "property of (j+1)^th item. A brown arrow points to "t_j" from the bottom right with the annotation, "j^th item" on the arrow.

The equation on the right:
X_i = 1/(Sigma{i=1}N Sigma{j=1}M_i(l^j_i/l^max))

N is in a purple box and we see a purple arrow pointing to it with the annotation, "number of objects" on top of the arrow. M_i is in a blue box with a blue arrow pointing to it with the annotation, "number of other objects" on the arrow. l^j_i is in a brown box with a brown arrow pointing to it and the annotation, "size of j^th service" on the arrow while l^max is in a green box and a green arrow pointing to it (from below) with the annotation, "maximum obj size" on the arrow.

Re: encyption

@juliank I think etebase solves this by encrypting everything client-side. the mains downsides are that

  1. calendars/contacts/other stuff cannot really be shared with other users (this should be theoretically possible, e2e file sharing services like Tresorit can solve it, but the etesync protocol doesn’t handle it nevertheless)
  2. it doesn’t really speak *DAV, but you need to run a bridge locally that actually handles the encryption. but afaik the Protonmail bridge for IMAP works similarly

orange site subtoot, finance, blockchain adjacent

the phrase ‘Turing-complete financial instruments’ should put horror into anyone who has studied computation, or ever had to debug a program blobfoxdisapprove

the phrase ‘financial instruments’ should probably also be terrifying, but for other reasons


turns out i managed to convince the examiners that i can speak french 🇫🇷

so much about this pointless (in CS) requirement (two CEFR accredited language exams) for obtaining a PhD in hungary blobfoxlaughsweat

Re: taking programming way too seriously, pointlessly long winded

@noracodes @nomemory

One way I like to think about programs (I got this brain worm from some summer school on probabilistic programming, I think) is that programs are described by finite terms, but the semantics of terms (defined by structural induction and least fixed points) form some nontrivial \omega-complete partial order when ordered by termination. Which is just abstract nonsense for

  1. programs should be described in a finite way
  2. you should be able figure out what a program means by looking at their parts and composing them in prescribed ways
  3. it should be possible to compare programs by which inputs they terminate on, provided their outputs agree on all inputs they both terminate on
  4. composition should be continuous: a program should terminate if all its parts terminate (in parallel, in sequence, or in whatever way the semantics define composition)

after copious amounts of handwaving, this should exclude anything that cannot be executed on a computer (programs with infinite descriptions, or cases when you have to take a non-least fixed point over something infinite – but ltps exist by the Kleene fixed point theorem). but allows expressing the lambda calculus, so it captures all Turing machines

crucially, non-continuous semantics, where a program terminates if a part of it doesn’t terminate is excluded. this encodes the sore lack of a halting oracle

HTML would be excluded because the underlying \omega-cpo is trivial, I think (any HTML page can be rendered in finite time, so there is no meaningful way to compare them by termination). CSS would probably be excluded because the CSS selector language is cleverly crafted to always evaluate in a finite number of steps

the beauty of looking at programs in this way is that this makes clear that the analysis of programs cannot merely depend on their syntax: any sufficiently interesting analysis will have to look at the underlying semantical category, which has much richer structure! handwave, handwave blobfoxwave by Turing and Rice we know it is so rich in fact that it’s hopeless to provide a general algorithm for program analysis!

in any other case, where analysis would be possible by just looking at the syntax of terms, we’re facing data (or configuration)

not as if any of this matters for the present topic: humans are rarely practically interested in programs that never terminate in convoluted ways. if it gets stuck in mundane way, like in a loop, we just get bored after a while and figure out enough to just close it

but while creating data or configuration can easily be so complex we’d be better off not to bother, only programs can theoretically provide unfathomably impossible complexity blobfoxwhoaa

(nevertheless, I’d expect the complexity faced day-to-day by someone writing “data” in HTML, CSS, Datalog, etc. roughly comparable to someone writing Lisp, C, Java, Haskell, Prolog or anything else outside of mathematical fun times)

Re: pleroma, long

@clonejo Hi! It’s relatively simple, you can just configure :mrf_simple in prod.secret.exs. First, I think you must make sure that the policy is actually enabled, that would be something like

config :pleroma, :mrf,
  policies: [
  transparency: false

(set transparency to true to to list the instances you block publicly on /about. include any other MRF policies you want in policies, such as Pleroma.Web.ActivityPub.MRF.ObjectAgePolicy. see for more details)

Then you can configure the policy itself, such as

config :pleroma, :mrf_simple,
  reject: [

to completely reject all activities from the listed instances.

The configuration is relatively straightforward once you get the hang of the Config Elixir module that is used to store instance configuration. Take a look at config.exs to see what are the actual defaults that you’re overriding in prod.secret.exs, the documentation might be a bit spotty on that part.

time to mask systemd-pcrphase-sysinit.service blobfoxsad

trying out the newly merged webfinger patches in pleroma. hope it won’t cause any federation issues, but make my activitypub handle prettier blobfoxnerd

arch linux, mostly self-inflicted

if space runs out on a btrfs filesystem while pacman is working, it’ll be a bad time, and it’s probably a much better idea to restore a snapshot (which caused the space to run out in the first place) instead of trying to paccheck everything

re: javascript

@rysiek btw, this is a bit silly, but could a service worker just use sendmessage to communicate with the main page which hosts an RTCDataChannel in lieu of instantiating an RTCDataChannel itself?

this idea comes from the fact that the current API (as implemented by Safari) needs a webpage to establish the RTC channel, which then gets sent to the worker (and probably only lives as long as the page is open). so in practice, the worker first has to serve some kind of shim webpage and script, which establishes the channel and sends in to the worker – then the worker could use the channel to answer further requests

so the silly thing to do would be to (in absence of RTC channel transfer support) establish the channel in the shim webpage, and notify the worker of this fact via a message. subsequently, on any fetch request the worker would send a message to the webpage, and the webpage would answer with another message transferring some buffer with the request data. this is of course completely backwards, but FetchEvent.respondWith does take any promise, and Response objects can be created from scratch (albeit with some CORS caveats)… blobcatscience

@midzer @fribbledom

re: javascript

@rysiek looks like the newest webkit is supporting transferring RTCDataChannel to a service worker: although I imagine that’s not very useful atm, since other browsers completely lack support, and RTC connections cannot be created in the worker itself at any case

you’re probably already familiar with the relevant webrtc issue: which explicitly highlights peer-to-peer content delivery as a use-case. interestingly, the last comment says that transferring to a service worker is not yet implemented even in safari, but things seem to have changed since then according to wpt

unfortunately, google seems to have blessed their http3-only webtransport as a way to open datagram connections in workers, which doesn’t support peer-to-peer connections at all. so I wouldn’t hold my breath for service worker webrtc support in chrome blobfoxsad

@fribbledom @midzer

overview of the Montreal skyline in daylight from the Mount Royal Chalet overview of the Montreal skyline in daylight from the Mount Royal Chalet. the Jacques Cartier Bridge is visible on the left

web, proprietary software

why is chromium / edge text rendering on windows so ugly? ablobfoxree

i’m working on a projects that requires all three of codium, eclipse, and intellij to edit. blobfoxdarkghostspooky


trying to buy a (small, but still larger than most computer monitors) tv without surveillance or ads 2022 challenge


i’m at the point where i have no clue whether the state management approach i tend to use with #reactjs is

  1. totally common
  2. frowned upon to the point that support for it might be removed from react at any time
  3. the scariest thought of it all: both blobfoxdarkghostspooky

#react #javascript #mobx