3 ms·

I would love to hear more about these "weird applications of type theory". Any references?

• electronvolt 9y ago
  So it turns out you can basically use type theory to encode a surprisingly large number of desirable traits about your program. (Caveat being that as you get more restrictive, you reject more "good" programs at compile time--no free lunch with Rice's theorem.) For example: In this paper, they basically use types (with an inference algorithm) to catch kernel/user pointer confusion in the Linux kernel. (https://www.usenix.org/legacy/event/sec04/tech/johnson.html https://www.usenix.org/legacy/event/sec04/tech/johnson.html) It turns out you can encode a lot of other interesting properties in a type system (esp. if you're building on top of the existing type system), though--you can ensure that a java program has no null-dereference checks (https://checkerframework.org/ https://checkerframework.org/ has a system that does this), and Coq uses its type system to ensure that every program halts (as a consequence, though, it isn't actually Turing complete). There's also cool things like Lackwit (http://ieeexplore.ieee.org/document/610284/ http://ieeexplore.ieee.org/document/610284/) which basically (ab)used type inference algorithms to answer questions about a program ("does this pointer ever alias?", etc.).