they are trying really hard to turn the DSA discord into a forum which does raise the question as to why the DSA discord isn’t a forum
i agree, it IS better if every discussion has a separate thread. what if there was a software which did this for you
yes, i know there is also Zulip
@Lady would rather not
@aescling oh do you have zulip takes
@Lady i have used it fur a small about of time because the Lean commewnity uses it fur all discussion and it felt about as bad to use as slack
@Lady research language with full dynamic types (not the same concept as dynamic typing) and tactic based purrogram writing (itself built in the language’s extensive metaprogramming features)
it’s fur nerds
@Lady the purrimary audience rn is the niche of mathematicians who want to rigorously formalize the field
@aescling i thought mathematicians already proved 100 years ago that it is impossible to rigorously formalize anything
@Lady that is not exactly what the incompleteness theorem says
@Lady well i guess it depends on what you think rigorous formalism is
@Lady anyway by “furmalize the field” i mean “extremely rigorously prove the accepted body of mathematical knowledge”, a purroject most actual mathematicians are not interested in fur many reasons, among them being that actually truly rigorous purroof is very tedious lol
@wallhackio @aescling i don’t think math is useless i just think it is a humanities
@wallhackio @aescling the humanities? history, art, language, philosophy, and maths? these aren’t useless things but fool on you if you think they can prove anything about the world
@wallhackio @aescling “we use math to do physics” sure. we use english too. so what
@wallhackio @Lady @aescling no if you’d studied the humanities your leftover knowledge after you’d forgotten all the specifics would still be useful
@Satsuma @wallhackio @Lady @aescling empecé a decir que la secuencia de humanidades obligatoria que cursaba no me sirve para nada más que saber las respuestas de programas de quiz. pero me acordé de que el leer de las memorias de nabokov me dio una desconfianza fuerte de escritores buenes. también aprendí que Aquinas no tenía buena lógica. y que algunos hombres str8 cogen a otros hombres. resulta que me quedan muchos conocimientos útiles de esos cursos.
