Idris - First Steps
Writing my first dependently typed function in Idris.
I hate debugging code, so I try really hard to produce correct code in the first place. As a result one of my main interests is automatic program verification. Initially for me this meant unit testing, then design by contract, later exploring how the type system can improve correctness. I was luck enough to attend an introduction to Idris with Edwin Brady at Functional Kats Conf in September. Idris is a dependently typed language, this means that types are first class citizens, they can interact with and depend on values.
