Agda is a dependently typed programming language that supports formal verification. It is primarily used for writing correct and trustworthy software, as well as for mathematical proofs and research in type theory.

Hello, world code example:

module HelloWorld where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit renaming (⊤ to Unit)
open import Agda.Builtin.String using (String)

postulate putStrLn : String -> IO Unit
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

main : IO Unit
main = putStrLn "Hello world!"

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

Repositories on GitHub: 2,472