Hurrah, after years of procrastinating, I'm officially finally a homeowner.

I'm going to stick something to the wall with blu-tak and NOBODY CAN STOP ME!

It turned out it was a really silly bug in the compiler, so I'll blame the author of that. Which clown wrote that anyway.

Oh, right. Oops.

Show thread

Yes I've named the new Idris core after the professor from Bagpuss. Don't judge me.

Show thread

I'm trying to get linearity checking working in the new Idris core. This is how it's going so far:

Yaffle> plus (S Z) (S Z)
(S Type) : Nat

It's possible I've messed this up somewhere.

I might even be able to move on to the interesting bit soon...

Show thread

I've been making convoluted programs for adding up numbers since around 2000. Getting extravagant now, they have as many as five (count 'em, five!) figures. :idris:

I'll have the Pork, Haggis and Lasagne sausage please.

Apparently I'm not the first to mention this. Also, they thought it was funny too so left it alone. Some small reasons why I like this boozer...

I'm trying to organise my work space a bit better at home. By which I mean, I've just ordered a new table so I have even more flat surfaces to spread paper and gadgets on.

I refuse to believe that "stupid" is the appropriate English translation for "blöde".

Lucy always seems to be judging me when I get an answer wrong on Duolingo.

I should add that a) I got this wrong deliberately to demonstrate, and that b) I am getting old and so I am unable to take a screenshot without also accidentally turning the volume down.

I've just been reading the Daily Dracula. It's a marvellous idea, and instead of explaining I'm just going to point at draculadaily.substack.com/abou

It followed up with "Too Old to Rock'n'Roll, Too Young to Die " by Jethro Tull and I can't help wondering if it's judging me now.

Show thread

Apropos of nothing at all, my random playing of my mp3s has just reminded me that Wondrous Stories by Yes exists, and I thought I ought to share in case you'd forgotten too.

"Scottish Family Party: Pro-Family, Pro-Marriage, Pro-Life" - don't think I need to do too much more research on this one at least...

Show thread

They probably assume people vote based on national (by which I mean UK) politics. I suppose they're probably right.

Show thread

Still trying to work out who to vote for in tomorrow's local elections. The problem is that hardly any of the candidates seem very interested in campaigning.

Last time, thanks to STV, I was able to vote "anyone but the Tory". This time there are way too many independents with no internet presence and incumbents who assume they don't need to bother. Maybe I'll spoil my ballot. I bet they'll be quaking in their boots at the prospect.

If I had read all the stuff I should it would work by now. Oh well.

(Can I keep this up for a while? Let us see.)

Show thread

(if you can wait for me to make the thing work right. It might take a while to get all the bits to work like they should.)

Show thread

On last boost: we can prove stuff works and make it go fast at the same time.

Show older
types.pl

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