mio (@mio)

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

mio @mio@shrimp.mio19.uk

1mo

@liamoc What are the dreaded bots? Are they something powered by generative models?

1

0

Liam O'Connor @liamoc@types.pl

1mo

@mio i call llms and other generative AI tools the "dreaded bots"

1

0

1

0

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