Great news everyone! I finally talk about AI hype. Someone finally mentioned LLMs one time too many, and the reckoning is upon us:
https://ludic.mataroa.blog/blog/i-will-fucking-piledrive-you-if-you-mention-ai-again/
been taking more photos recently to try and counteract the staring at a screen all day
https://aria.rip/photos/Edinburgh.html
Julian: Hard work is not rewarded. It's exploited.
Conrad writes about our k8s plans for the SourceHut blog:
https://sourcehut.org/blog/2024-06-12-infrastructure-updates/
thinking of how formerly open source corporate like Red Hat or HashiCorp are migrating to more restrictive licenses because they don't want the Big 5 to appropriate their labour, while FOSS people still reject ethical and anti-capitalist licenses in favour of Freedom 0 dogma, even after being repeatedly backstabbed by Apple, Google etc. and after watching their free labour bankroll the likes of Anduril or the IDF.
@ltchen @gallais @me The current formalisation is extrinsically typed, meaning the evaluator has to explicitly prove each step is well-typed. With intrinsic typing you basically get this part for free, which can lead to things being cleaner (but this is somewhat subjective)
With that said I've been procrastinating finishing this for a while, and in the meantime wasm & spectec have moved a lot, so this is more of a hobby project.