Coq is a proof assistant and formal verification tool. Its main uses include the development and verification of formal mathematical proofs, program correctness, and specification of software systems.

Hello, world code example:

Require Import Coq.Strings.String.

Eval compute in ("Hello world!"%string).

Popularity: Less than 1% of developers are using or have used this language.*
*According to StackOverflow's 2023 survey.

Repositories on GitHub: 5,850