User avatar
Liam O'Connor @liamoc@types.pl
2mo
I find the proposed agda contributors policy to be quite disappointing. I'm not sure what I will do about this yet, and I'm not actively using Agda at the moment so i don't need to come to a decision now, but I'm leaning towards avoiding Agda as I currently avoid Lean (despite the fact that I like Lean quite a lot as a language, the dreaded bots have infected too much of its ecosystem and culture for me to have a good time engaging with it)
2
0
1
0
User avatar
mio @mio@shrimp.mio19.uk
1mo
@liamoc What are the dreaded bots? Are they something powered by generative models?
1
0
0
0
User avatar
Liam O'Connor @liamoc@types.pl
1mo
@mio i call llms and other generative AI tools the "dreaded bots"
1
0
1
0
User avatar
mio @mio@shrimp.mio19.uk
1mo
@liamoc I installed a software. There was a bug; I opened an issue. The reply from the developer was horrifically not distinguishable from dreaded bots. The reply contained so many hallucinations. But when I looked at some other posts from the developer, it felt like from a human. I just felt more disoriented than when facing with dreaded bots. I am trying to find a new word for it
0
0
0
0