News for hackers. Stuff that matters.

A comment on Ask HN: A well-typed program won't go wrong?.

Re:Ask HN: A well-typed program won't go wrong? by loumf on Monday November 03, 2014 @05:14PM (#8553909)
A well-typed program is isomorphic to a proof -- google "propositions as types". This is not the same as saying your program is correct.

For your specific question, google "dependent types", which are types that depend on a value.

In your case, Haskell can type check positive integers:

http://mvanier.livejournal.com/3820.html

[ Parent | on HN ]

There are no comments on this comment yet.