3 ms·

Formal methods/dependent types are the future in the same way fusion is, it seems to be perpetually another decade away. In practice, our industry seems to hav

Formal methods/dependent types are the future in the same way fusion is, it seems to be perpetually another decade away. In practice, our industry seems to have reached a sort of limit in how much type system complexity we can actually absorb. If you look at the big new languages that came along in the last 10-15 years (Kotlin, Swift, Go, Rust, TypeScript) then they all have type systems of pretty similar levels of power, with the possible exception of the latter two which have ordinary type systems with some "gimmicks". I don't mean that in a bad way, I mean they have type system features to solve very specific problems beyond generalizable correctness. In the case of Rust it's ownership handling for manual memory management, and for TypeScript it's how to statically express all the things you can do with a pre-existing dynamic type system. None have attempted to integrate generalized academic type theory research like contracts/formal methods/dependent types. I think this is for a mix of performance and usability reasons that aren't really tractable to solve right now, not even with AI.

nyssos 3y ago
> If you look at the big new languages that came along in the last 10-15 years (Kotlin, Swift, Go, Rust, TypeScript) then they all have type systems of pretty similar levels of power, with the possible exception of the latter two which have ordinary type systems with some "gimmicks". Those are very different type systems: - Kotlin has a Java-style system with nominal types and subtyping via inheritance - TypeScript is structurally typed, but otherwise an enormous grab-bag of heuristics with no unifying system to speak of - Rust is a heavily extended variant of Hindley-Milner with affine types (which is as "academic type theory" as it gets)
- mike_hearn 3y ago
  Yes, I didn't say they're the same, only that they are of similar levels of power. Write the same program in all three and there won't be a big gap in level of bugginess. Sometimes Rustaceans like to claim otherwise, but most of the work in Rust's type system goes into taming manual memory management which is solved with a different typing approach in the other two, so unless you need one of those languages for some specific reason then the level of bugs you can catch automatically is going to be in the same ballpark.
  - nyssos 3y ago
    > Write the same program in all three and there won't be a big gap in level of bugginess. I write Typescript at work, and this has not been my experience at all: it's at least an order of magnitude less reliable than even bare ML, let alone any modern Hindley-Milner based language. It's flagrantly, deliberately unsound, and this causes problems on a weekly basis.
    - mike_hearn 3y ago
      Thanks, I've only done a bit of TypeScript so it's interesting to hear that experience. Is the issue interop with JavaScript or a problem even with pure TS codebases?

nyssos 3y ago

> If you look at the big new languages that came along in the last 10-15 years (Kotlin, Swift, Go, Rust, TypeScript) then they all have type systems of pretty similar levels of power, with the possible exception of the latter two which have ordinary type systems with some "gimmicks". Those are very different type systems: - Kotlin has a Java-style system with nominal types and subtyping via inheritance - TypeScript is structurally typed, but otherwise an enormous grab-bag of heuristics with no unifying system to speak of - Rust is a heavily extended variant of Hindley-Milner with affine types (which is as "academic type theory" as it gets)

mike_hearn 3y ago
Yes, I didn't say they're the same, only that they are of similar levels of power. Write the same program in all three and there won't be a big gap in level of bugginess. Sometimes Rustaceans like to claim otherwise, but most of the work in Rust's type system goes into taming manual memory management which is solved with a different typing approach in the other two, so unless you need one of those languages for some specific reason then the level of bugs you can catch automatically is going to be in the same ballpark.
- nyssos 3y ago
  > Write the same program in all three and there won't be a big gap in level of bugginess. I write Typescript at work, and this has not been my experience at all: it's at least an order of magnitude less reliable than even bare ML, let alone any modern Hindley-Milner based language. It's flagrantly, deliberately unsound, and this causes problems on a weekly basis.
  - mike_hearn 3y ago
    Thanks, I've only done a bit of TypeScript so it's interesting to hear that experience. Is the issue interop with JavaScript or a problem even with pure TS codebases?