4 ms·
With rich types, you can get rid of the correct bugs, too. You can encode an arbitrary amount of information into a verified, proven specification. The specif
by Peaker 13y ago
With rich types, you can get rid of the correct bugs, too.
You can encode an arbitrary amount of information into a verified, proven specification.
The specification is orders of magnitude smaller and simpler than the actual code, so much easier to get correct.
- agentultra 13y agoI've heard that before. "Proven," in as far as you trust the axioms and assumptions made by the Haskell compiler. It's an important distinction because you must assume that the 50k lines of C code that get compiled and statically linked into your Haskell programs is also, "correct," by extension despite it living outside the set of axioms and assumptions your program has been proven within. Don't get me wrong, Haskell is a neat language, I just don't accept its trade-offs for most of the work I do.
- codygman 13y agoThat's certainly a valid opinion, but I believe you may be doing yourself a disservice by not trying to use Haskell in some of that work you do. However I can't say that for sure yet, I'm still evaluating how useful Haskell is for me in my "real world" tasks. Thus far I've been able to accomplish things rather easily, but I don't believe I've written enough to form a solid opinion yet. As far as the Haskell compiler living outside of that set of axioms and assumptions my program has been proven with, that is something that does needle me a little but it seems to be a smaller hole than most languages are working with.
- Peaker 13y agoSure, you'll hit an underlying platform bug, once in a few years, whether in the RTS or the OS.. But you'll prevent orders of magnitude more bugs that would waste your time debugging in the best case, or hit production in a slightly worse case.