Agda
https://twitter.com/agdakx/status/1577952310243872769?s=20&t=UJrepWvNkFpXFRNY8yoWDA agda2hs blog post jasper
Martin Escardo Introduction to Univalent Foundations of Mathematics with Agda
Programming Language Foundations in Agda
apt-get install agda agda-mode agda-stdlib
echo 'module hello-world where
open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String)
postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
main : IO ⊤
main = putStrLn "Hello world!"
' > /tmp/hello-world.agda
cd /tmp # Why do I have to do this? Me dunno.
agda --compile /tmp/hello-world.agda
./hello-world