Benjamin C. Pierce writes what it is like to use a proof assistant to teach programming language foundations.
Software has become ubiquitous. It’s all around us and in us. It is in our pockets, in cars, airplanes, stock exchanges, our bodies, our offices and in lots of other places. As a computer scientist and a programmer I’ve worked in aeronautics, computer security, finance and automotive industry and I can say that software engineering is a mess. The Atlantic demonstrates this point rather thoroughly in an interesting piece on the state of the software engineering profession. I agree with the article and here I will briefly tie this to what I see to be a solution, split into four parts: 1) the licensing of professional software engineers, 2) a requisite degree in computer science, 3) mandatory formal methods in software development, and 4) all software should be free as in freedom.
Just this morning these two books landed my mailbox:
The Little Typer is a new book on dependent type theory, written by Daniel P. Friedman, an author of The Little Schemer, and David Thrane Christiansen, an Idris contributor. Verified Functional Programming in Agda is a book by Aaron Stump, on using dependent types in Agda to prove various properties of programs. After having read the Type-driven Development with Idris book by Edwin Brady, I am hoping these two books will significantly expand my knowledge of and improve my skills in type theory, theorem proving and typed functional programming. Looking forward to reading the books! If you haven’t noticed by now, I got hooked on dependent types!
Software testing has been an important, if not prevalent way of checking software correctness. In this article I will tell how have my doctoral dissertation on testing and verification of imperative software as well as my work experience after the studies led me to typed functional programming, which consequently gave me a different perspective on automatic software testing. Furthermore, I’ll explain why functional programming and static type systems are important for software correctness.
Philip Wadler makes a fun note about today’s programming languages: “Most of you use programming languages that are invented, and you can tell, can’t you?” I recommend watching his whole talk Propositions as Types!
For fast searching of source code that avoids peeking at your build files use the ag tool from Debian’s silversearcher-ag package, like this: ag -s –haskell “what” where.
I stumbled upon a recording of a talk by George Wilson on the monad transformer library (MTL) in Haskell. He goes on to demonstrate how monad transformers can be made more composable by using constraints instead of directly putting a monad transformer in the return type of a function. What is presented there is definitely an improvement, however it is still unsatisfactory. In particular, in his examples there is no separation of describing and running a program, which means everything happens in the IO monad (the MonadIO constraint in function signatures in the examples). In other words, anything goes and such functions are again too powerful.
In case you are a Haskeller interested in learning Idris, check out a short list of things to look out for.