Trellys aspires to be a functional programming language with full dependent types, general recursion, and a sound logical fragment.