«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple

«Which is usually as interesting as the program itself.» And ten times as hard to write. Not just saying that — I spend most of my time in Agda, and even simple things are rather difficult. But I think this will improve as we learn the right way to look at things.