Making Wrong Code Look Wrong (2005)

Re:Making Wrong Code Look Wrong (2005) by lifthrasiir on Saturday November 09, 2019 @09:57PM (#21496120)

I think in this particular case they suffice, because they are clearly different subtypes as I've mentioned.

It is much harder, if not impossible, if you have to describe a relation between two or more values of the same subtypes. For example, imagine that you already "know" certain indices never go off the boundary of given array but want to encode that information to types. Sure, there exists a Rust crate [1] that tracks a relation between indices and originating array via lifetime, but it is complicated.

[1] https://github.com/bluss/indexing

[ Parent | on HN ]

Re:Making Wrong Code Look Wrong (2005) by touisteur on Sunday November 10, 2019 @02:33AM (#21496913)

Mmmh thanks for the link and the paper about generative types. Seems very interesting!

I'm wondering if using type predicates or type invariants (+ proof for static verification, otherwise the check will mostly be at runtime) would help here.

Look up https://blog.adacore.com/spark-2014-rationale-type-predicate... if interested.

[ Parent | on HN ]