Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Sound type systems help you prove things. In other words, a type system is a tool that partially discharges part of the programmer's proof obligation. Of course, what you can't prove, you still need to test. This isn't news to anyone.

The problem is when the programmer doesn't know how much of his proof obligation is actually discharged by his use of the type system. (Hint: Not all of it!) And the solution is educating programmers, not replacing types with tests.



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

Search: