Is there any space focused on software engineering in Lean?

Stream: new members

[Blue]

I'm interested in Lean exclusively as a programming language, because of it's metaprogramming capabilities.
I have no interest in theorem proving of any sort, not even proving properties of my programs.

Due to my goals I perceive some cultural friction when interacting with Lean users. Everyone has always been extra welcoming and nice, but there's a big gap which affects every conversation I have: we talk about the same things using a different language (which makes mutual understanding harder), we find that the interesting or difficult bits are different, we have different preferences and styles, we value different things, about code written in Lean.

I've noticed a similar cultural barrier with other functional programming languages as well. As a native speaker of C++ it's hard to communicate with most Haskellers, for instance.
But with Lean this feels much stronger. I haven't met any other Leaner yet who has a complete lack of interest in proofs. Even in this Zulip, the "metaprogramming" channel is mixed in with "tactics". Even the Leaners who describe themselves primarily as programmers, seem to be mainly interested in theoretical computer science, which lives on the ridge between math and software engineering IMO.

Is there any space, group, community or channel focused mainly on using Lean for software engineering, while ignoring the proof-related capabilities of Lean?

[Ray Myers]

Hi @Blue, I'm fairly new and not the right one to speak for the community's needs, but since I'm also closer to the software engineering side I figured I'd chime to show there is some interest.

I've been in the industry 17 years and have been learning Formal Methods for the last year. Admittedly what draws me to Lean is the verification capabilities, that's the only reason I could picture trying to understand a language with dependent types tbh - but maybe that will be more normal someday. Still, I use Lean to model the design of real production code and I'd love to use it as an implementation language at some point too.

You're probably aware that one of the main Lean books is programming-focused: Functional Programming in Lean. It's a good start, better than exists for most other provers. Aside from having very sophisticated meta programming as you mention, another benefit that doesn't require proofs is that even encoding something in a "provable" language tends to make it somewhat rigorous. Exhaustive pattern matching and various other features make it more natural to avoid bugs by default. (Most ML-family would have these benefits, like Haskell, Gleam, OCaml, Elm).

If someday it becomes normalized to code in a proof-aware language, then that would make the job of verification so much easier. So you're on the frontier but I think there's promise.

[Kim Morrison]

Users who aren't interested at all in verification are of course very welcome! There isn't currently a channel "Programming in Lean", but it seems pretty reasonable that we should create one.

It would be unreasonable to forbid discussion of verification or proofs there (e.g. sometimes even "pure programming" applications care about a proof for performance sake, e.g. to avoid runtime array bounds checks!) but it might still help achieve what you are looking for.

[nrs]

I think a "Programming in Lean" channel would be nice!