Correctness – A paradigm for sustainable software development

Re:Correctness – A paradigm for sustainable software develop... by tombert on Friday April 05, 2019 @10:57AM (#19583155)

I think it's experimental right now, but Idris (which I consider the "Child of Haskell"), has basic support for linear types [1], which could at least help the space-prediction problems. Doesn't hurt that Idris isn't lazy-by-default either.

My point is that I actually think that Idris could end up being successful in an industrial sense, due to the fact that it gives you all the correctness guarantees of Haskell (and more), but has managed to (thus far) avoid a lot of the cruft that has built up in the ~30 years Haskell has been around. Fingers crossed.

[1] http://docs.idris-lang.org/en/latest/reference/uniqueness-ty...

[ Parent | on HN ]

Re:Correctness – A paradigm for sustainable software develop... by newacctjhro on Monday April 08, 2019 @12:37AM (#19602142)

This stuff feels like a proof of concept that isn't really integrated to the rest of the language (Kinda like OCaml's OO). For example, it's unfortunate that Type, UniqueType and BorrowedType are different kinds (in Rust, they are the same kind; stuff that isn't "unique" just implement Copy)

Rust's advantage is that its borrow system, with reborrowing rules and such, feels much more ergonomic.

[ Parent | on HN ]

Re:Correctness – A paradigm for sustainable software develop... by tombert on Monday April 08, 2019 @10:31AM (#19605522)

You're not wrong, but the fact that some work is being done on this is at least a good sign I think. A proof-of-concept is necessary before you can integrate these things organically into the language, and I that as a result it could be pretty interesting.

If I knew anything about elaborate type systems, I would try and address your complaints. Sadly, my knowledge of linear logic and whatnot is very ad hoc.

[ Parent | on HN ]