Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.
Benjamin C. Pierce writes what it is like to use a proof assistant to teach programming language foundations.
Someone said: “I doubt there’s any more useful way to group programming languages than by the kind of bullshit their users are happy to put up with.”
As of last week I’ve finally gave the Scala programming language a try, as in I’ve actually started coding in Scala. I don’t want this to be a yet-another way of writing plain old imperative, hence next to incomprehensible and unmaintainable code. Therefore, lately I’ve been putting a lot of energy into thinking how to program functionally. You can say I’m finally delivering on my earlier promise to code in Scala. In other words, seeing lots of bad/imperative code during an internship can do you good, i.e. it can make you want to program in a better way. Continue reading