3 ms·

I'd agree that people are generally going to be less familiar with type theory (though I think it's not uncommon to touch on the simply typed lambda calculus in

I'd agree that people are generally going to be less familiar with type theory (though I think it's not uncommon to touch on the simply typed lambda calculus in undergrad courses), but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it (though maybe you meant that you immediately started writing specifications of large, real-world systems in TLA+, but I'd presume you'd then be the outlier on that). In my experience people pick up Isabelle (/HOL) really quickly and writing specifications in a type theory based proof assistant isn't a huge jump from that. Now, writing actual proofs is a completely different matter, but I didn't disagree with you on how economical/ergonomic the over all approach actually is, just the basic complexity of the theory/specifications ;) >What is the type of its first argument? Some universe U, which is an implicit argument. You could alternatively write your Lean example as def id {u} {α : Sort u} (a : α) : α := a Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? Similar to how one could make those generics explicit, it is actually possible to define a special type of all universes (not including itself). Agda does this by having a special primitive type of universe levels. As an example id : forall {u : Level} -> forall {A : Set u} -> A is the signature of the universe polymorphic identity function. The Level type doesn't you any issues because it is essentially a 'top' type that doesn't have a type itself.

pron 6y ago
> but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it That has not been my experience. Typed formalisms have further complications with "partial" functions -- either they're actually partial, which is a rather complex concept, or you need refinement types to define them, as well as with constructive mathematics, which isn't necessary for specification. Plus, what are you going to do with your specifications after a few hours if you can't write proofs after few hours (or a few days)? And because of that the tutorials don't and won't just teach specification first and proof later -- as the TLA+ tutorials do -- so even if this were hypothetically true, you have nowhere to learn things like that. Lean has very good tutorials, and you can compare how far they get how quickly with the TLA+ tutorials. I don't know if it's even possible to teach such formalisms the same way as TLA+, but even if it were possible, I haven't seen such tutorials. Those languages are so infused with their formalism's proof theory that it's hard to separate the two [1]. For example, most typed formalisms define integer division by zero to equal zero. Suppose they didn't, and they wanted to teach how to define division "properly". How much would a student need to know in order to define and use the div function? OTOH, TLA+ handles partiality in what I think is a simpler way, with a careful definition of Hilbert's epsilon operator (see https://pron.github.io/posts/tlaplus_part2#the-choose-operator-and-the-meaning-of-undefined https://pron.github.io/posts/tlaplus_part2#the-choose-operat...) Finally, most specifications people in industry are interested in are not of sequential algorithms but concurrent ones, which you also can't do after a few hours (or a few days). > In my experience people pick up Isabelle (/HOL) really quickly Depends what you mean by "really quickly." Isabelle has some accidental complications such as the nested languages. But I think something like Why3 can be picked up quickly, although it doesn't handle concurrency easily. > Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions. I call them subroutines, but those that call them functions know (I hope) that they're overloading the term. In any event, students that do learn simply typed lambda calculus learn it in the context of programming languages whose type systems are inconsistent and they certainly don't learn how to do maths with them. Anyway, `id` is not a function in Lean because the universe argument doesn't have a type. But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? [1]: Which I think is a big problem. The clean separation of model and proof is an important property of a formal logic designed for ease of learning, expression and comprehension, and we must not forget that ease of learning, expression, and comprehension -- so that practitioners rather than logicians will be able to make everyday use of it -- has been a central goal of formal logic since at least Frege, if not Boole or even Leibniz, equal in importance to, if not superseding, that of mechanical proof. I might be getting carried away, but I think that TLA+ is a pretty special accomplishment in the history of formal logic in that it is perhaps the first truly rich formal logic that is commonly used by non-specialist practitioners in their day-to-day work.
- ImprobableTruth 6y ago
  If you're fine with 'stupid' refinement types in the form of subset types without coercion, not only do you get them 'for free' from the core type theory without introducing another language element, I personally also think they're quite intuitive. Using a subset type of non-zero nats or providing a proof that the argument isn't zero to define a 'proper divsion' just 'makes the most sense' in my opinion, but that may just be ultimately down to personal taste. I really do think though that no single part of dependent type theory is actually all that complex. It's not as simple as TLA+, but there's nothing really hard about it till you start proving. And I'm not saying that all this is feasible right now, but I'm fairly certain that this is at least fundamentally possible. You can't 'truly' separate specifications from proofs in dependent type theory, but you also definitely don't need to really understand how to write actual proofs to write even complex specifications in it. All of this of course depends on stronger automation for a good subset (possibly by also integrating strongly with other provers), but I don't think that's a total pipe dream (though I am definitely personally biased on this). >The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions I'm just talking about the 'well-behaved' subset, but let me go at this from another angle. If Lean tomorrow introduced a Sort Omega to type universes, the set of programs that you can write wouldn't change. It's essentially just a syntactic change. Would that really be enough to make you say that these are functions now while they previously weren't? >But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? If you quantify over a universe, a constraint gets introduced as part of the type checker. These constraints can be viewed as a graph that is checked for cycles, so not having a specific universe isn't an issue.
  - pron 6y ago
    > but I don't think that's a total pipe dream You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a model and its proof theory aesthetically unappealing (not that I find everything in formal FO set theories appealing). Of course, it may have other advantages. > Would that really be enough to make you say that these are functions now while they previously weren't? Yes, provided that `id` wouldn't be a function that could operate on that type. But any operator with a truly universal domain cannot be, itself, a quantifiable object without introducing a Russell paradox (perhaps constructiveness can save it, but assuming the system allows non-computable objects, too). As it is, `id` is universal, but it isn't a function. This isn't just a philosophical or even a purely syntactic difference. Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. > so not having a specific universe isn't an issue. Does that require forbidding full recursion, or can you still introduce non-computable objects?

pron 6y ago

> but I really think anybody who has all those prerequisites could also learn enough type theory to write specifications in a couple hours because you don't actually need a deep understanding of type theory to use it That has not been my experience. Typed formalisms have further complications with "partial" functions -- either they're actually partial, which is a rather complex concept, or you need refinement types to define them, as well as with constructive mathematics, which isn't necessary for specification. Plus, what are you going to do with your specifications after a few hours if you can't write proofs after few hours (or a few days)? And because of that the tutorials don't and won't just teach specification first and proof later -- as the TLA+ tutorials do -- so even if this were hypothetically true, you have nowhere to learn things like that. Lean has very good tutorials, and you can compare how far they get how quickly with the TLA+ tutorials. I don't know if it's even possible to teach such formalisms the same way as TLA+, but even if it were possible, I haven't seen such tutorials. Those languages are so infused with their formalism's proof theory that it's hard to separate the two [1]. For example, most typed formalisms define integer division by zero to equal zero. Suppose they didn't, and they wanted to teach how to define division "properly". How much would a student need to know in order to define and use the div function? OTOH, TLA+ handles partiality in what I think is a simpler way, with a careful definition of Hilbert's epsilon operator (see https://pron.github.io/posts/tlaplus_part2#the-choose-operator-and-the-meaning-of-undefined https://pron.github.io/posts/tlaplus_part2#the-choose-operat...) Finally, most specifications people in industry are interested in are not of sequential algorithms but concurrent ones, which you also can't do after a few hours (or a few days). > In my experience people pick up Isabelle (/HOL) really quickly Depends what you mean by "really quickly." Isabelle has some accidental complications such as the nested languages. But I think something like Why3 can be picked up quickly, although it doesn't handle concurrency easily. > Not being able to specify the type of u in Lean might seem kinda cheaty, but I'd say that's similar to how one declares generic type parameters in e.g. Java. You wouldn't say that those languages' generic functions aren't actually functions, would you? The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions. I call them subroutines, but those that call them functions know (I hope) that they're overloading the term. In any event, students that do learn simply typed lambda calculus learn it in the context of programming languages whose type systems are inconsistent and they certainly don't learn how to do maths with them. Anyway, `id` is not a function in Lean because the universe argument doesn't have a type. But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? [1]: Which I think is a big problem. The clean separation of model and proof is an important property of a formal logic designed for ease of learning, expression and comprehension, and we must not forget that ease of learning, expression, and comprehension -- so that practitioners rather than logicians will be able to make everyday use of it -- has been a central goal of formal logic since at least Frege, if not Boole or even Leibniz, equal in importance to, if not superseding, that of mechanical proof. I might be getting carried away, but I think that TLA+ is a pretty special accomplishment in the history of formal logic in that it is perhaps the first truly rich formal logic that is commonly used by non-specialist practitioners in their day-to-day work.

ImprobableTruth 6y ago
If you're fine with 'stupid' refinement types in the form of subset types without coercion, not only do you get them 'for free' from the core type theory without introducing another language element, I personally also think they're quite intuitive. Using a subset type of non-zero nats or providing a proof that the argument isn't zero to define a 'proper divsion' just 'makes the most sense' in my opinion, but that may just be ultimately down to personal taste. I really do think though that no single part of dependent type theory is actually all that complex. It's not as simple as TLA+, but there's nothing really hard about it till you start proving. And I'm not saying that all this is feasible right now, but I'm fairly certain that this is at least fundamentally possible. You can't 'truly' separate specifications from proofs in dependent type theory, but you also definitely don't need to really understand how to write actual proofs to write even complex specifications in it. All of this of course depends on stronger automation for a good subset (possibly by also integrating strongly with other provers), but I don't think that's a total pipe dream (though I am definitely personally biased on this). >The type system in Java or Haskell cannot be used as a sound mathematical foundation, so whatever I call those things it would mean something quite different from maths functions I'm just talking about the 'well-behaved' subset, but let me go at this from another angle. If Lean tomorrow introduced a Sort Omega to type universes, the set of programs that you can write wouldn't change. It's essentially just a syntactic change. Would that really be enough to make you say that these are functions now while they previously weren't? >But I wonder, in Agda, is `id id` some object even when a specific universe cannot be inferred? If so, how does Agda avoid Russel's paradox? If you quantify over a universe, a constraint gets introduced as part of the type checker. These constraints can be viewed as a graph that is checked for cycles, so not having a specific universe isn't an issue.
- pron 6y ago
  > but I don't think that's a total pipe dream You may well be right. Personally, though, I find this essential inseparability of the logic as specifying a model and its proof theory aesthetically unappealing (not that I find everything in formal FO set theories appealing). Of course, it may have other advantages. > Would that really be enough to make you say that these are functions now while they previously weren't? Yes, provided that `id` wouldn't be a function that could operate on that type. But any operator with a truly universal domain cannot be, itself, a quantifiable object without introducing a Russell paradox (perhaps constructiveness can save it, but assuming the system allows non-computable objects, too). As it is, `id` is universal, but it isn't a function. This isn't just a philosophical or even a purely syntactic difference. Lean doesn't allow you to refer to `id` as an object, just an application of it to a known universe. > so not having a specific universe isn't an issue. Does that require forbidding full recursion, or can you still introduce non-computable objects?