general topologists will literally make up a space and be like "HEY ISN'T THIS FUCKED UP"

if the first result that shows up when you google something is an nlab page, it's not basic

@wilbowma so for the first result, we know that our synthesis algorithm is sound. it cannot implement anything that doesn't satisfy the tests. it can be *maliciously compliant*, but it will always have the right signature.

it is not complete. it will simply not halt if it can't find an answer. however, we can put a max size on the program, and if it can't find a solution with, say, 5 nested conditionals or something wild like that, we can safely say there's an issue.
it isn't perfect at detecting inconsistent sets of unit tests, but it's Good Enough to be useful.

hazel 💤 boosted

also could hypothetically give me the funniest reason ever for changing my name

Show thread

honestly maybe i should just pick a different name. i have other reasons but this is one of them

Show thread

every time i see someone talk about hazel (the structure editor) i do like. a triple take. a quadruple take

i'm at probably the worst mental low i've been in for years, so if my responses are sparse that's why. sorry

Rust protip: if you have cyclic data, have you considered not having cyclic data?

oh wait you need it? uhh... uhhhhhh

Why say "fighting the borrow checker" when you could say "being owned by ownership"

@justinfrank @petrichor I guess this is the problem with systems programming as a whole, is that you can't really make a clean break between the way data is stored and the way you think about the data.

hazel 💤 boosted

@petrichor @justinfrank Right, allocation is allocation, whether it happens in literal memory or inside a data structure you make inside that memory

@justinfrank I feel like the Rust experience with anything self-referential is someone saying "that's a bad design choice", and then refusing to say how else to do it

Since, yeah, it's a bad design choice. The ownership type system inherently does not work with this kind of thing. But sometimes you just gotta

Show older

hazel 💤's choices:

types.pl

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