I should be a bit more active on here again. So, here goes: I've had a cold for two and a half weeks now and i think it's finally starting to go away after I got some antibiotics.

I used the holidays and the sick leave to brush up on my Swedish again with an online teacher.

If I happen to reach someone who speaks Swedish via follower power (unlikely, but can't hurt to try), I'd be happy for someone to practise with casually. I can offer German and Esperanto in return.

New paper! "Verifying an Efficient Algorithm for Computing Bernoulli Numbers"

As a case study, I took the most efficient algorithm known for computing Bernoulli numbers and verified the hell out of it, and then Peter Lammich refined it all the way down to efficient LLVM code.

Not quite as fast as the original unverified C++ code, but that's not because verification is hard but rather because I'm bad at optimising x86 assembly at that level. 😅

Will be presented at ITP in Reykjavík next week.

https://doi.org/10.4230/LIPIcs.ITP.2025.35

I just learnt that for some reason, the Wikipedia article on the Fisher–Yates shuffle cites my formalisation of it in the Archive of Formal Proofs. Guess that explains why that entry keeps getting cited by papers that have absolutely nothing to do with formalisation. 😄

https://www.isa-afp.org/entries/Fisher_Yates.html
https://en.wikipedia.org/wiki/Fisher%E2%80%93Yates_shuffle

https://mastodon.gamedev.place/@pikuma/114004127295465108

I basically taught myself programming with Borland Delphi 7. The nostalgia! 😍

Although to be perfectly honest my first programming language was actually Visual Basic Script. It's… pretty terrible. But you can just open a text editor, save the thing as .vbs, and run it. No compiler or anything.

*sigh*

Time to put another €10 into the "struggled for quite some time to prove something that blatantly isn't true" jar.

https://math.stackexchange.com/a/5013353/67576