In my post about where I intend to go with this blog for the next little while, I mentioned that I wanted to work with the Scheme programming language. However, I gave it some more thought and I decided against it for two reasons. The first reason is that the scheme specification drama is just a mess. I have no interest in deep diving into a flame war and coming out with a language I'd most likely be partially unsatisfied with. The second reason is that since I have ambitions towards working with and creating dependently typed programming languages, I thought I'd give Lean, the hot new dependently typed language on the block, a test drive.
The Lean programming language is pretty much exclusively known for mathlib, its most popular library that contains proofs for more math than most people ever learn due to a lot of attention given by the broader math community. However, Lean was developed with general purpose programming in mind. There appears to be efforts being made towards creating a standard library and there's also a guide on how to do functional programming with this language. I just started fumbling around with this guide and so I thought I'd share my first hello world program in lean.
I'll be sharing code in the following form and refer to these forms as "files" that live in a "repository":
A hello world program in Lean is very simple to write. Since that's the case, I'll also showcase some file structure, string interpolation, and comments in lean.
I'm aware that this syntax is closely related to how haskell does things but I'm not yet prepared to go into detail about how this works. I hope to do so in the future!