4 ms·

When I last looked into Lean, I was highly unimpressed, even for doing math proofs. There's no way I'd invest into as a general-purpose language. Idris at leas

by bmitc 2y ago

When I last looked into Lean, I was highly unimpressed, even for doing math proofs. There's no way I'd invest into as a general-purpose language. Idris at least does state that they what people building real programs with it and don't want it to just be a research language. For dependent types, I myself am skeptical about languages trying to continuously push more and more stuff into types. I am not certain that such efforts are a net positive on writing good software. By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. Highly typed languages force more and more effort into pre-compile time and you will often find yourself trying to fit a problem into the chains of the type system. Rather, I think reasonably multi-paradigm languages like F# are the sweet spot. Just enough strict typing and functional core to get you going for most of your program, but then it allows classes and imperative programming when those paradigms are appropriate. I think the way to go to write better software is better tooling and ergonomics. I don't think type systems are going to magically save us.

tsimionescu 2y ago
> By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. While I generally share your skepticism, I think this is quite wrong. A good part of the point of advanced type systems is to make more complex problems possible while still being well typed. For example, in C, if you want a function whose return type is tied to an input argument's type, you either use void* and casts (no type safety), or you don't write that function. In languages with even slightly more advanced type systems, you can write that function and still get full type safety. Even more advanced type systems achieve the same things: you can take programs that can only be written in a simpler type system and make them safe. In standard Haskell, for example, you can't write a Monad and actually have the compiler check that it respects the Monad laws - the implementation of Monad functions just assumes that any type that implements the right shape of functions will work as a monad. With dependent types, you can actually enforce that functions designed to work with monads only apply to types that actually respect the monad laws. The trade-off with very complex type systems is different, in my opinion: after some point, you start duplicating your program's logic, once in the implentation code, but again in the type signatures. For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs.
- User23 2y ago
  I think GP's point was that most[1] programs that can be represented will fail to please the programmer or his principals. The act of programming is navigating the state space of all possible programs and somehow finding one that has the desired properties and also doesn't otherwise suck. When viewed through that lens, a type system preventing most programs from being represented is a good thing, since odds are every single program it prevents is one that is unpleasant or otherwise sucks. [1] of the countably infinite possible programs, virtually all
  - auggierose 2y ago
    That would make sense if writing a program would be similar to randomly drawing a program from a pot of programs. If instead I have a good idea what I want to write, the type system may either guide me towards the solution, or hinder me. It usually hinders me, I don't need a type system to guide me, but I like a type system that can check for trivial errors (oh, I meant to pass a list of numbers, not just a single number).
- IshKebab 2y ago
  > For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs. Not to mention the tools to debug complex type errors are generally much less mature than the tools to debug runtime errors. But even so, I think we could still benefit from going a little further towards the "proof" end of the type system spectrum in most cases. I don't think anyone really wants to deal with Coq and similar, but having used a language with dependent types for integers and vector lengths it's really nice to be able to say stuff like "this integer is in the range [0, 8)" and then have it catch errors when you pass it to a function that expects [0, 3) or whatever.
a57721 2y ago
> When I last looked into Lean, I was highly unimpressed, even for doing math proofs. I remember exploring different proof assistants for the first time in the 2000s. Back then, only people with a background in logic were involved, and most of the proofs that were formalized as showcases were of textbook results from the 19th century at most, or some combinatorial stuff like the four-color theorem. I believe Voevodsky was one of the first prominent non-logicians to become interested in proof assistants, using Coq around 2010. Nowadays, several mathematicians coming from algebraic geometry, number theory, etc. are promoting formal proofs, and it seems like most of them have chosen Lean. I don't know whether this is because Lean is somehow better suited for working mathematicians, or if it was simply a random personal preference among people who got enthusiastic about this stuff and started advertising it to their colleagues? I am not familiar with every proof assistant out there, but many of them are a very hard sell for mathematicians and lack a comprehensive math library. Lean seems to be one of the few exceptions.
- nextos 2y ago
  Isabelle also has a fairly large set of mathematical proofs and supporting libraries, see https://www.isa-afp.org https://www.isa-afp.org. People routinely publish new proofs there, it is actually a regular referred journal.
ykonstant 2y ago
>When I last looked into Lean, I was highly unimpressed, even for doing math proofs. There's no way I'd invest into as a general-purpose language. Can you elaborate? I am using Lean as a general-purpose language writing simple little programs, so I have not encountered the deeper parts of the runtime etc. I'd like to see some criticism/different perspectives from more experienced people.

by bmitc 2y ago

tsimionescu 2y ago

> By their very definition, the more typed a language gets, the less programs it can represents. That obviously reduces buggy programs, but it also reduces non-buggy programs that you can implement. While I generally share your skepticism, I think this is quite wrong. A good part of the point of advanced type systems is to make more complex problems possible while still being well typed. For example, in C, if you want a function whose return type is tied to an input argument's type, you either use void* and casts (no type safety), or you don't write that function. In languages with even slightly more advanced type systems, you can write that function and still get full type safety. Even more advanced type systems achieve the same things: you can take programs that can only be written in a simpler type system and make them safe. In standard Haskell, for example, you can't write a Monad and actually have the compiler check that it respects the Monad laws - the implementation of Monad functions just assumes that any type that implements the right shape of functions will work as a monad. With dependent types, you can actually enforce that functions designed to work with monads only apply to types that actually respect the monad laws. The trade-off with very complex type systems is different, in my opinion: after some point, you start duplicating your program's logic, once in the implentation code, but again in the type signatures. For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs.

User23 2y ago
I think GP's point was that most[1] programs that can be represented will fail to please the programmer or his principals. The act of programming is navigating the state space of all possible programs and somehow finding one that has the desired properties and also doesn't otherwise suck. When viewed through that lens, a type system preventing most programs from being represented is a good thing, since odds are every single program it prevents is one that is unpleasant or otherwise sucks. [1] of the countably infinite possible programs, virtually all
- auggierose 2y ago
  That would make sense if writing a program would be similar to randomly drawing a program from a pot of programs. If instead I have a good idea what I want to write, the type system may either guide me towards the solution, or hinder me. It usually hinders me, I don't need a type system to guide me, but I like a type system that can check for trivial errors (oh, I meant to pass a list of numbers, not just a single number).
IshKebab 2y ago
> For example, if you want to specify that a sort function actually sorts the input list, you might find that the type specification ends up not much shorter than the actual code of the function. And apart from raw effort, this means that your type specifications start being large enough that they have their own bugs. Not to mention the tools to debug complex type errors are generally much less mature than the tools to debug runtime errors. But even so, I think we could still benefit from going a little further towards the "proof" end of the type system spectrum in most cases. I don't think anyone really wants to deal with Coq and similar, but having used a language with dependent types for integers and vector lengths it's really nice to be able to say stuff like "this integer is in the range [0, 8)" and then have it catch errors when you pass it to a function that expects [0, 3) or whatever.

a57721 2y ago

> When I last looked into Lean, I was highly unimpressed, even for doing math proofs. I remember exploring different proof assistants for the first time in the 2000s. Back then, only people with a background in logic were involved, and most of the proofs that were formalized as showcases were of textbook results from the 19th century at most, or some combinatorial stuff like the four-color theorem. I believe Voevodsky was one of the first prominent non-logicians to become interested in proof assistants, using Coq around 2010. Nowadays, several mathematicians coming from algebraic geometry, number theory, etc. are promoting formal proofs, and it seems like most of them have chosen Lean. I don't know whether this is because Lean is somehow better suited for working mathematicians, or if it was simply a random personal preference among people who got enthusiastic about this stuff and started advertising it to their colleagues? I am not familiar with every proof assistant out there, but many of them are a very hard sell for mathematicians and lack a comprehensive math library. Lean seems to be one of the few exceptions.

nextos 2y ago
Isabelle also has a fairly large set of mathematical proofs and supporting libraries, see https://www.isa-afp.org https://www.isa-afp.org. People routinely publish new proofs there, it is actually a regular referred journal.

ykonstant 2y ago

>When I last looked into Lean, I was highly unimpressed, even for doing math proofs. There's no way I'd invest into as a general-purpose language. Can you elaborate? I am using Lean as a general-purpose language writing simple little programs, so I have not encountered the deeper parts of the runtime etc. I'd like to see some criticism/different perspectives from more experienced people.