Jons Mostovojs @jonn@social.doma.dev

Oh no https://github.com/sudo-project/sudo/commit/6aa320c96a37613663e8de4c275bd6c490466b01 #sudo

https://youtube.com/watch?v=4AB8YakmBWM&feature=share
⚠️🇺🇦Rescue efforts underway after Russian missile hits civilian apartment block in Uman, Ukraine (Kanal13 - Azeri News in English VIDEO) #Ukraine #Azerbaijan #NATO #Press #News #Invasion #Russia #9yearsOfWarInUkraine #WantedDeadOrAlive

As an aside, let me add that ethnic cleansing is as American as pie. I strongly recommend everyone read Loewen's "Sundown Towns", which carefully documents a hidden era of ethnic cleansing across America. And looks at how the cultural traditions linger. I think it's essential for understanding the age we're in, the second Nadir. https://www.amazon.com/Sundown-Towns-Hidden-Dimension-American/dp/0743294483

Reading about #bluesky, it's impressive to me how little Jack has learned.

As somebody who (briefly) worked at Twitter on anti-abuse, the place is a goldmine of lessons on fucked-up behavior. And the CEO comes out of the cryptocurrency space, which also has a rich history of garbage people run wild.

But instead of something that applies any of that, they have apparently produced the same sort of tired neoliberal marketplace-of-ideas horseshit product that Twitter was to start.

(a thread)

The safest thing to be during a Russian missile barrage is a military target.

*tap* *tap* Is thing thing on? 🎙️

@jonn turns out "Navalny LIVE" channel has an entire 15-minute story with that person, on how bad things were for him at prison. Not only it is absolutely uncritical, but they're even doing fucking close-ups of the wagner promo posters https://youtu.be/jRjjQ7PC7Sg?t=98

RT @lesiavasylenko
#putin launches 23 missiles on #Ukraine tonight, and @Pernod_Ricard decides to re-launch sales of @jamesonwhiskey to #russia. Guess #kremlin needs more money to kill more Ukrainians 🤷‍♀️ @GarretAhearn thank you for raising this issue in #Ireland

Yesterday, Jonathan Brouwer defended his master thesis on implementing dependently typed languages in the Spoofax language workbench. You can find the pdf at https://repository.tudelft.nl/islandora/object/uuid%3A7bf3c0f5-71fb-4e08-bcdb-1c873c7e1e63

I was really pleasantly surprised at the nice things that modern language workbench technology has on offer, and would definitely consider it when prototyping a new language. The main drawback is the limited control over how implicit arguments are solved, but since a prototype will often not even have implicits, even a basic unifier is nice to have.

One thing I'm still missing is a way to export the specification of the type system to a proof assistant so I can prove things about it. Perhaps Statix2Agda would be a nice topic for another master thesis?