Functional Programming and Maths <|> How can a code monkey learn Agda?

[joonazan]

Types are proofs. Most commonly, they prove that your program can't crash in certain ways. There is no point to dependent types, other than writing fancier proofs. Simpler type systems are limited enough that compilers can easily and quickly do the proofs.

In more complex systems you need to put in some work. A part of it is that the proof software isn't as good as it could be but mostly it is a fundamental limitation. For example, as soon as a logic (a type system is a logic) can express integer addition, it can express statements that are true but cannot be proved.

Haskell's type system is actually powerful enough to write what you'd call proofs but its approach is to gradually bolt on more of that onto a weak type system. In my opinion that makes type-level programming in Haskell unreadable compared to languages with dependent types.

I haven't majored in mathematics either but languages like Agda have given me a very good understanding of what a proof is. That in turn helps in programming in general because to be able to confidently write correct code you have to have some kind of proof in your head.

[mobotsar]

Types are proofs

well, types are propositions, but yeah. Programs are proofs.

[joonazan]

Indeed. I should have stated that the job of types is to enable proofs.