Bots in the list of contributors

[NChechulin]

There are 6 entries of bots in the list. 4 of them are dependabot and the other 2 are bors. All of them have [bot] at the end of their names.
Maybe we should consider excluding them from the list?
Or, alternatively, we could write their developers' names. But this is controversial, as they're probably developed by a group of people. Also, it's much harder to do from a technical point of view.

[Mark-Simulacrum]

I would be unopposed to tagging them as bots explicitly (e.g., with the [bot] suffix), but I don't think excluding them makes sense at this time -- I would rather not filter these lists at all.

[steveklabnik]

Robots are people too.

(We historically have explicitly kept bots in the list. I would oppose removing them. I would prefer not to tag them, but wouldn't try to block it if people really wanted.)

[CleanCut]

If the purpose of the contributors list is to recognize and appreciate people's efforts, then I am in favor of removing the bots from the contributors list.

Anthropomorphizing bots is whimsical and can be fun, but people appreciate being recognized while bots do not. It might be fun to count bots separately (maybe a different sort of stats list), but it feels to me like we devalue contributors when we implicitly suggest that a piece of code that we set to a task perpetually deserves more recognition and appreciation than humans putting in their time and effort to develop Rust.

It might make sense to include bots in a page that was more stats-oriented, but this page seems more focused on recognizing and appreciating people's efforts than emitting statistical counts of artifacts.

[nnethercote]

Robots are people too.

I'm a hard disagree on that, at least for the bots relevant to this discussion.

I have a similar opinion to @CleanCut: in a list designed to celebrate the contributions of humans, it is kinda gross that the #1 spot permanently belongs to a bot.

Marking bots clearly (and with a link to an explaining footnote of some kind) would be an improvement. Filtering out bots entirely would be even better, because currently you have to mentally subtract one from everyone's ranking to account for bors.