@Wno-all I could create badges with only 101 reputation. I think anyone can in private beta.

Nobody (not even mods) can create a tag without an appropriate question for it to go on.

@NikeDattani I followed AB's twitter

@ice1000 Oh, you're saying that you found this site via Andrej Bauer's Twitter. When I said "how are you finding it", I meant, "how are you enjoying the site?" :)

@VisualMelon Not bad. Do you have experience with using Theorem Provers?

@NikeDattani I was obviously referencing tag badges, which you can create with 101 reputation if you post really insightful answers to one kind of question while getting huge numbers of downvotes everywhere else.

@wizzwizz4 I'm not sure if anything here is "obvious"! By tag badges, do you mean the bronze, silver and gold ones that people get once they've answered enough questions and got enough upvotes on those answers?

@NikeDattani Yeah; they're created when they're earned for the first time, if the badge numbers are anything to go by.

(But it was actually a mistake; I did mean to say tag.)

@NikeDattani you can tell from my activity. Basically, it's awesome.

Is this site also supposed to be about formal proof systems (that aren't necessarily implemented as proof assistants)? If so, I've got a load more questions.

@wizzwizz4 I would be inclined to say formal proof systems can be discussed here...after all, they're the theoretical underpinnings of theorem provers.

@wizzwizz4 It's "supposed" to be about theorem provers, but I agree with @AlexNelson that questions about the underpinnings of theorem provers are on topic.

@wizzwizz4 The name tag badges is used in the SE software for badges awarded for enough answers in some specific tag. They can only be awarded if a tag has at least 100 questions and the user needs at least 20 (non-CW) answers in that tag.

Of course, that's just terminology - probably it's not that important.

@NikeDattani Not really; I had a mathematician colleague who was keen to use Agda for some formalisations, so I helped him with that, and I've messed around with F* but never had any real use for it. Hoping this stack might give me some ideas as to how I can put it to use, and help me maintain some sort of awareness of what is going on in this field.

@GuyCoder I wasn't supposed to respond. Sorry

@wizzwizz4 Thank you, this was indeed where my question came from. I was not able to add {guidance,tag} info to a newly created tag, not so sure about how everything here works - yet.

@Wno-all You have to wait a little bit for tags to go through.

Especially when lots of people are creating lots of tags.

@HenryWHHackv3.0b No worries. We can still delete comments as needed. Unless someone else adds a comment.

Questions, answers, edits, comments and votes are the only instant things on Stack Exchange. Reputation points are only mostly instant, and everything else is scheduled.

Makes sense. That's okay too, this is a beta after all.

BTW: How is the new private beta going?

The funny thing I realized is that if someone wants to use those for lyrics there is nothing stopping others from using the same for another song. It is all CC BY-SA 4.0

I hate to be this guy but I think if you're new to the topic of proof assistants you should refrain from closing questions, like this one: proofassistants.stackexchange.com/questions/281/…

It's relevant to the implementation of proof assistants based on type theory, which are dependently-typed languages, where proof checking is type checking.

@Li-yaoXia Thumbs up emoji.

@Li-yaoXia I was kinda shocked and disappointed to see that thread closed, it seems like an ideal question for PA.SE.

@GuyCoder a quick reminder that your Agda questions still have no other answers (:

@ice1000 Fair enough. I will take a look.

Gave them both an accept vote. Thanks for answering.

Just curious: Any example of a function that provably terminates but is extremely hard to define (i.e. convince the termination checker) in a proof assistant?