Pinned toot

hey-hey, I'm new on this instance! Currently doing a PhD at TU Delft w/ @agdakx at PL group. Mostly working on surface-level features of dependently-typed languages.

In the past I've done some work with (Meta)Coq and Iris, but not so much these days. I also was in the industry for a little while.

Your fellow Ukrainian 🇺🇦.
In my previous life I was into experimental music and typefaces, but these days your chances of finding me on a weekend are highest at a protest.

Dana boosted

And you have a conversation with someone
And they seem to undestand
And they wish you "relaxed and festive holidays"
And you go along with your day counting the explosions in Kyiv this morning

Show thread

Computer-assisted proofs, tired: coq, lean, isabelle
Computer-assisted proofs, wired: G A L A C T I C A ™️

Dana boosted

Niki and Wouter interviewed me on the Haskell Interlude podcast, the episode is out!

haskell.foundation/podcast/18/

In the meantime, if someone knows how to generate module graphs painlessly for a package build with cabal2nix, I'm all ears

Like, the setup I have is dead simple:
```
let defpkgs = <pinned nixpkgs rev>
in {nixpkgs ? defpkgs}: nixpkgs.pkgs.haskell.packages.ghc922.callCabal2nix "packageName" ./. {}
```

And then shell.nix is essentially
```
let pkg = import defpkgs.nix {}
in pkg.env
```

I suppose the simplicity is why I keep thinking generating module visualization should be easy here

Show thread

As one does, I gave up.

I'm sorry graphmod-plugin and haskell-nix-plugins. I'm sure you work for someone.

In the meantime I can drop into a shell with regular graphmod and get the info I need.

Show thread

oh no please send help im in the nix world again but this time with haskell source plugins and i dont understand anything 😭​

Another meta-observation on fediverse incoming.

This isn't my first attempt to get rooted in fediverse, but the first one that feels less like a niche for people already interested in fedi on its own and more like a new general-public platform.

And in that way, this is the first "general public" social network experience I'm participating in that's not corporate-owned.

While others have mentioned very welcomed lack of *the algorithm*, what makes my spider-senses tickle is the lack of a walled garden.

In a sense that the previews of the posts are pretty good when you post a link to a toot elsewhere. Links themselves aren't forwarded through some corporate-owned link shortener. Instances don't block you from viewing a post and responses if you don't have an account.

This surprised me but also spoke for the fact that while I thought I was aware of the dark patterns of walled-gardens, it still "got to me".

So the change of pace is very refreshing and welcome.

hey-hey, I'm new on this instance! Currently doing a PhD at TU Delft w/ @agdakx at PL group. Mostly working on surface-level features of dependently-typed languages.

In the past I've done some work with (Meta)Coq and Iris, but not so much these days. I also was in the industry for a little while.

Your fellow Ukrainian 🇺🇦.
In my previous life I was into experimental music and typefaces, but these days your chances of finding me on a weekend are highest at a protest.

types.pl

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