Correctness – A paradigm for sustainable software development

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 ]