> More refined, my claim is that it is a super powerful tool that brings substantial benefits. And that it's a mistake to not use this tool.
I mostly agree with this. I wouldn't say it's super powerful, but it's a super convenient tool that quickly eliminates a broad class of errors without that much effort or contortions in our programs. I do think that the sweetspot for types is something like OCaml or Rust, and that going even into Haskell style (monads) starts to expend too much effort on the types compared to functionality.
I am hopeful that other techniques will come along and complement types to more easily statically check more complex properties of our code. I've been hearing great things about TLA+ style property-based specifications that I'd like to try at some point.
> For instance, there's the Rust crate dfdx, which uses dependent typing to encode the shapes of tensors. [1]
I don't think shapes of tensors is a particularly complex property. It's nice that this is enforced, but I still see it in the area of very simple properties. Rust's borrow checking is actually a better example of a more complex property of a program being statically verified.
> This isn't quite right. At least, I think what you're saying is that "physics proofs don't set up typing rules therefore they don't use types." But then again, proofs aren't necessarily programs. Is every physics proof computable? I'm not a physicist so I'll defer that to an expert.
Physics is basically all about computation, and very little about proof. The point of physics is usually to compute a property of a physical system based on some model, then perform an experiment and measure the same property. If the measurement agrees with the computation, that's a "proof" that the model is "correct" (in quotes because of course these are not what we normally mean by those words in formal contexts).
And in those computations, physicists don't use types in any way you might see in a computer science paper in their computations. Measurement units are somewhat similar at a very high level, but they are used very differently in practice.
Thanks for a very thoughtful reply! (Feels like real HN. I appreciate that.)
It seems like we're not in too much disagreement. I also see Rust's borrow checker as a real engineering achievement. They were able to take lessons learned discovering affine type systems and apply in in a way that gives Rust programs some tremendously wonderful properties. Whether it's making sure that the ML code doesn't do something invalid or whether all of the code doesn't make memory errors, I still see a never-ending march of progress on investing more into type systems and static analysis.
I appreciate your insights on Physics. I understand enough that Quantum Physics takes the view (more or less, I believe!) that the universe is akin to a computer, with particles (bits) that behave in specific ways and determine how everything works (computation, if I can continue the metaphor).
I replied to your linked comment. But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a
> a property of a physical system based on some model
counts as a value that has a type. Perhaps the whole understanding is that Physics has a _very complex type system_. Perhaps one that no one has invested in trying to make computable?
Yes, I think we agree quite a bit, and for me as well this is exactly the type of conversation I come to HN for.
I replied more in depth on the measurement units post on the specifics about that, so I'll leave it aside here.
> I appreciate your insights on Physics.
About physics though, I would say that when I'm talking about computations I'm not describing some complex or deep idea about the universe acting as a computer. I just mean that most of what you do as a physicist is simply to do computations, much like we would in school. You don't write proofs the way most mathematicians do: you take some functions (say, Newton's laws of motion) and an initial state, and compute the state of the system after some time or at some event. Your result is not a proof that X = Y, it is simply the value Y, which you didn't know beforehand. Ideally, you might write a program that automates this work for you, so that instead of doing a computation by hand, you ask a computer to do it for you.
> But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a
>> a property of a physical system based on some model
> counts as a value that has a type.
I don't think this is the right way to look at it. Types are a specific concept in computer science/math and they act in certain ways. They are for example isomorphic to propositions in first order logic (the Church-Howard correspondence if I remember correctly), but that doesn't mean they are the same thing.
I mostly agree with this. I wouldn't say it's super powerful, but it's a super convenient tool that quickly eliminates a broad class of errors without that much effort or contortions in our programs. I do think that the sweetspot for types is something like OCaml or Rust, and that going even into Haskell style (monads) starts to expend too much effort on the types compared to functionality.
I am hopeful that other techniques will come along and complement types to more easily statically check more complex properties of our code. I've been hearing great things about TLA+ style property-based specifications that I'd like to try at some point.
> For instance, there's the Rust crate dfdx, which uses dependent typing to encode the shapes of tensors. [1]
I don't think shapes of tensors is a particularly complex property. It's nice that this is enforced, but I still see it in the area of very simple properties. Rust's borrow checking is actually a better example of a more complex property of a program being statically verified.
> This isn't quite right. At least, I think what you're saying is that "physics proofs don't set up typing rules therefore they don't use types." But then again, proofs aren't necessarily programs. Is every physics proof computable? I'm not a physicist so I'll defer that to an expert.
Physics is basically all about computation, and very little about proof. The point of physics is usually to compute a property of a physical system based on some model, then perform an experiment and measure the same property. If the measurement agrees with the computation, that's a "proof" that the model is "correct" (in quotes because of course these are not what we normally mean by those words in formal contexts).
And in those computations, physicists don't use types in any way you might see in a computer science paper in their computations. Measurement units are somewhat similar at a very high level, but they are used very differently in practice.
I go into a little more detail on this in [0].
[0] https://news.ycombinator.com/item?id=38692762