Hacker News Reader

Comment by mrkeen | Hacker News Reader

I'm so lost.

(I'm firmly in the static-typing camp, coming from an internal philosophy of "computers are supposed to do things as fast as possible, and not make mistakes".)

> Intrinsic types are great because you are guaranteed to have a mathematically-sound safety net at all times.

Sounds great, even if I take it with the usual grain of salt.

> Extrinsic types are useful because you can apply multiple type systems to your code

If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n?

View on HN

This is actually a rare instance of the grain of salt being unnecessary. Depending on the type system, it is possible for it to guarantee that the only source of error be in your specification and not in your implementation.

> If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n?

I don't it is intended to imply that extrisic type systems wouldn't be sound.

As for why you'd want several type systems, one benefit I imagine is that different type systems could verify different aspects of your program, instead of forcing to cram everything into one type system.

Afaik just because type system is sound doesn't alone mean that it can be used practically to prove every interesting property of a program.

This lets different parts of your code use different type systems, so to speak, by picking and choosing which annotations you specify. Another real-life example is the “unsafe” mode some statically-typed languages have, which effectively switches to a laxer type system.

> Another real-life example is the “unsafe” mode some statically-typed languages have, which effectively switches to a laxer type system.

Are you referring to Rust here? Because I believe unsafe there doesn't change type checking or type system in any way

“Unsafe” disables borrow checking in Rust, which is part of the type system. C# also has a (different) “unsafe”.

Conceptually speaking they are quite close: both let you write code C-style with raw pointers within unsafe blocks. Similar to Rust, C# also has a subset of Unsafe and Marshal APIs which explicitly indicate their risk for bypassing compiler or language checks when either you know what you are doing or when whatever goal they achieve is not expressible with safe code.

unsafe does not disable the borrow checker, it allows calling functions that could not be otherwise written in code that is OK'd by the borrow checker.

Reply on news.ycombinator.com