[grumblenum]

> focusing purely on type- and memory-safety, not conformance to arbitrary specifications

What are types if not arbitrary specifications? Are you suggesting that formally verified software is not memory safe? What on earth does "scalable" even mean? A verified program cannot scale? If not, why not?

[zozbot234]

Types are not 'arbitrary' in any real sense. Type systems can be described as a sort of formal verification that leverages and is closely aligned with the syntax structure of actual code, thus type systems can preserve compositionality but don't generally support non-local reasoning, at least not in a very elegant way. This is exactly what can make them potentially more scalable than other sorts of FV, hence more useful for programming "in the large".

[grumblenum]

Types that can be defined by users are, necessarily, part of a language syntax, so that they are aligned with the syntax is just a tautology. Equating user defined types with formal verification is just nonsense. C has types. Python has types. Rust has types. That the program does what you think it should do does not logically follow the mere existence of types. I have no idea what "in the large" is supposed to mean. I feel like GPT-3 is arguing with me.

[PhaseLockk]

Maybe I can try to explain the parent comment's point a different way. When saying that rust works on types and not on arbitrary specifications, I think he is saying that rust is more limited than languages that support arbitrary specifications. However, by making this tradeoff it achieves a reasonable degree of safety without incurring a ton of overhead.

I believe the comment that types are aligned with the syntax is meant as a contrast to other languages which include specifications written in a format substantially different from or fully removed from the implementation. This can reduce the friction of using type-based verification when compared to formal verification capable of describing an arbitrarily complicated spec.

When discussing the scalability of types, I think he is saying that because types are coupled to the implementation, and don't support non-local reasoning, it is less likely that you will run into issues with type checking as you try to compose many small components into a larger program. In contrast, my impression is that with full formal verification, it can become extremely difficult to properly verify a large system.

Regarding your comparison to C and python, I think it's clear that the parent was comparing the specific type system and borrow checker that Rust provides vs. formal verification, not making a statement about the general concept of a type system. In particular, I don't think it's reasonable to assume he was saying the existence of types provides any sort of safety. Rather, it's clear he was saying the use of a powerful type system (such as that found in Rust or Haskell) to implement a limited specification of the program functionality can provide a degree of safety.

[marshray]

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

"In other words, the Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects.

If one abstracts on the peculiarities of either formalism, the following generalization arises: a proof is a program, and the formula it proves is the type for the program."

[wtetzner]

I believe what zozbot234 is saying is that Rust focuses on a specific subset of formal verification, and on trying to make a language with that enforces that subset in a way that is still somewhat ergonomic.

I'm assuming "scalable" in this case is referring to the fact that fully verifying a piece of software is currently takes a large amount of effort. Rust's approach is more "scalable" in the sense that they decided to focus primarily on memory safety, and punted on other forms of verification in the hope that it would be more ergonomic/require less effort.