← Back to context Comment by epgui 10 hours ago Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs. 2 comments epgui Reply hyperhello 10 hours ago Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it. mswphd 8 hours ago it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.
hyperhello 10 hours ago Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
mswphd 8 hours ago it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.
Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.