News for hackers. Stuff that matters.

A comment on Why is Rust difficult?. Parent comment

Re:Why is Rust difficult? by GolDDranks on Monday January 22, 2018 @03:06AM (#16202706)
I think they mean something like what proof assistants like Cog and Irdis do. ATS is another language that enables proofs, and it's more geared to the systems programming use case, as it's similar to C.

Note that unit tests prove only that the code works for those inputs and those code paths tested. Mathematical proofs are supposed to be exhaustive.

[ Parent | on HN ]
Re:Why is Rust difficult? by jwhite on Tuesday January 23, 2018 @09:35PM (#16219874)
Sorry this comment is so late; ATS is also interesting because it has linear types that allow compile-time resource tracking similar to Rust's ownership and lifetime tracking. If you use linear types you can opt out of the garbage collector. That makes it very attractive for systems programming, and in particular embedded systems. I believe there is a demo of ATS running on an Arduino of some sort.

I haven't had the time to learn it yet, though I would like to.

[ Parent | on HN ]