went down the road of trying out js_of_ocaml with HTML canvas today… then discovered that you can't turn off anti-aliasing in canvas

having a bunch of fun with Processing for some generative art stuff after a long hiatus (trying to go back to basics and remember where I came from) but… lets just say I'm remembering again why I went looking for alternatives to Java all those years ago hah

@borko consisted of a random assortment of grumps I have developed with Rust over the years

“My personal list of Rust grievances”

Posted a collection of toy language implementations a couple of days ago (arithmetic expressions and a couple of dependent type systems). Have a bunch more I want to play with, but perhaps it is useful for someone? github.com/brendanzab/language

Just know that developing a language is SOOOO hard. and really easy to just post off a bunch of random thoughts if you don't need to try to figure out how they all fit together in practice.

In a mild panic this afternoon as a random gist I posted a year ago gets shared with a decent portion of the programming internet. 😬

I also kind of look back at my… 7 years in full time programming stuff in amazement. How did I get here... what am I doing

some proof trees to go with your gum trees

@brad idk kind of feel a bit odd boxing myself in though… so might eventually look for other places. Just wanted to get off the big instance. The local timeline is nice though!

@brad btw this is my new account hehe

@liamoc hah, ain't that always the case!

@liamoc Is the order of the premises important?

@liamoc cool, I'll give this a go!

@liamoc Ahh cool! I feel better now hehe. I had a suspicion that it might be an issue with Holbert. I realise I might be pushing it a bit hard, so it's inevitable these things will pop up!

@liamoc I seem to be getting stuck on some of the proofs related to applying (lambda (x . x))… wondering if my rule for beta-reduction (ie. function/computation( apply ( lambda _ ) _ )) is at fault? I seem to get into a state where I can't make any progress :(

@liamoc Anyway, is now updated the main gist with universes: liamoc.net/holbert/?https://gi (after dodging some rate limiting from github).

I'm now getting schooled by a bunch of homotopy type theorists in why Tarski style universes are cool/better, heh. Learned so much from Holbert already… just feel I understand a bunch more how things fit together now, and can now ask a bunch more questions.

@liamoc ended up editing the JSON by hand hehehe

@liamoc Now I'm thinking that the stuff to do with universes belongs at the end in a single section hahaha… oh no

@roundcrisis This one is goofy and old but interesting: github.com/pandaman64/effectiv - uses generators to build an algebraic effect system in Rust.

There's also been some recent work on ‘contexts’ which seem related to effects:
- tmandry.gitlab.io/blog/posts/2
- blog.sunfishcode.online/contex

There's more stuff out there on contexts though, probably worth looking around for more info.

Show older

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