Constructive Type Theory is Hard but People Want It

“What every software developer should know”: I’m not going to list them here, but in my own current exploration into the various crevices of computer science, I’m finding it amazing how the software development industry is constantly rethinking of what has been around a long time.

The latest experience with this is a post “I want to fix programming” which I found from a response to it “Yep, Programming Is Borked”.

There is a comment that mentions Coq. Which is in the right direction since both of those posts are hinting at what is ultimately constructive type theory or intuitionistic type theory. So, yet again, we have someone posting: “we need X” and X has been worked on by researchers for 30 years.

My guess is that they don’t realize just how hard it is to do what he suggests. Having a “compiler” construct something to match his description of the result of a sort would be extremely difficult. Here’s a 24 page write up of how to get the proofs–and not automated, it requires user interaction–in order to do just addition.

I wonder if it would raise the overall state of the industry if everyone had a basic knowledge of all the things going on out there. Maybe there is just too much. I’m guessing that university programs don’t have survey type classes that cover the breadth of computer science. So we have graduates come out with large holes in their knowledge. Which is unfortunate since many who might contribute more take years to stumble across what they have been missing.

It’s kind of sad: in spite of being generally considered a “brainy” industry, the software world is extremely faddish, rehashes the same concepts again and again… You’d think we could find a way to be pushing steadily forward instead of so much sideways and circular.

Maybe I should put up a website that tries to just condense the high level topics and concepts that every developer should be aware of.

Comment on this post