I would have never believed it without seeing it with my own eyes in my own programs, but Haskell's B&D type system really helps a lot in producing correct prog

I would have never believed it without seeing it with my own eyes in my own programs, but Haskell's B&D type system really helps a lot in producing correct programs. I am a relatively incompetent Haskell programmer and I am constantly amazed at how often algorithms I implement turn out correctly after I finally get them to compile. It's an exaggeration to say that you must embed a proof of anything in your program. You just have to think a bit more carefully and explicitly about how your data is defined.