Hacker News new | past | comments | ask | show | jobs | submit login

I'm not sure what he had in mind at that time, but Dijkstra was never all that enthusiastic about type theory. He thought it was a promising and worthwhile avenue, but was suspicious of it being treated as a panacea.

http://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EW...

"Another thing we can learn from the past is the failure of characterizations like "Computing Science is really nothing but X", where for X you may substitute your favourite discipline, such as numerical analysis, electrical engineering, automata theory, queuing theory, lambda calculus, discrete mathematics or proof theory. I mention this because of the current trend to equate computing science with constructive type theory or with category theory."




> [Dijkstra] was suspicious of [type theory] being treated as a panacea

I'd be suspicious of anything being treated as a panacea.


=) Sorry, I was being sloppy there - couldn't come up with an accurate and un-platitudinous way to characterize Dijkstra's attitude. There are other places in his writings where he's suspicious of an overemphasis on types, I think his criticisms of Ada mention it for example.

Dijkstra was a big proponent of rigorous mathematical means of establishing program correctness in general, of course, but he didn't necessary equate that with types.




Consider applying for YC's W25 batch! Applications are open till Nov 12.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: