I can see the headline now... "Show HN: Pudding - A language for programming proofs". I could see a lot of uses for this kind of programming. In a language like Matlab or R, we just assume that the implementations correctly match the theoretical methods they implement, but anyone who has deleved into the internals of some published R library knows that's not always the case. With the expanded use of pure functional languages for more closely mapping method to implementation, proof programming could offer a useful form of unit testing to the development of libraries.