Formal verification is important for guaranteeing correctness of critical computer programs. LiquidHaskell and Idris are 2 functional programming languages in which formal verification can be performed using the respective type systems. This thesis investigates the differences between LiquidHaskell and Idris when verifying list functions, with respect to expressiveness, annotation overhead and type checking times. The used list functions, as well as their specifications consisting of correctness properties, were carefully selected. No large differences in expressiveness were found between LiquidHaskell and Idris. However, Idris was found to be better than LiquidHaskell without the automation feature PLE, regarding annotation overhead and type checking times. With PLE enabled, no large differences were found.

Formell verifiering är viktigt för att garantera korrekthet av kritiska datorprogram. LiquidHaskell och Idris är 2 funktionella programmeringsspråk där formell verifiering kan göras med hjälp av språkens typsystem. Denna uppsats undersöker skillnaderna mellan LiquidHaskell och Idris vid verifiering av listfunktioner, gällande expressiveness, annotation overhead och typechecking tider. De använda listfunktionerna och tillhörande specifikationer bestående av korrekthetsegenskaper, valdes omsorgsfullt. Resultaten visade inte på några stora skillnader gällande expressiveness mellan LiquidHaskell och Idris. Gällande annotation overhead och typechecking tider visades Idris vara bättre än LiquidHaskell utan automatiseringsfunktionen PLE. Med PLE visade resultaten inte på några stora skillnader.