11–20 of 40 posts
Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.
Minor thing. Purely as a side: in C and C++, the conditional statement is written using if and else, while the conditional expression is written with a ternary operator ? and :. ending a sentence with . is a must. Including a period directly after a syntactic construct about ? and : is .. jarring because it is possible to attempt to read this as :. as an atomic construct in the language. Or even worse, the three-dots…
> Also, I always find it interesting the ternary operation is constructed in statements/expressions in ? ... : notation but actually has "two" operators there. the ? is the conditional, the : is the binary-choice. It's a language syntax choice which "side" is true or false and it is also true that you can't construct statements in : without a prior ? but .. its hardly a single operator in syntax terms if it has two d…
I don't think "operator in syntax terms" is nearly as well-defined as OP thinks. Why couldn't `?` be parsed as half an operator and `:` as the other half? There's no rule that says a parser has to call each distinct symbol token its own "operator". In fact, I'd argue that the only reason this might seem seem like a rule is that almost all of the other operators in common use are either unary or binary, making it easy to use a single token for the operator itself. That's why it's called the "ternary operator"; it's the only one that operates on three things! The only alternative to spreading it out across separate tokens with an operand in between is to put multiple operands in a row on one side of it; as confusing as `foo ? bar : baz` might be, I have strong doubts that `foo ?: bar baz` would be less confusing in most real-world cases.
Earlier quoted context omitted.
> Also, I always find it interesting the ternary operation is constructed in statements/expressions in ? ... : notation but actually has "two" operators there. the ? is the conditional, the : is the binary-choice. It's a language syntax choice which "side" is true or false and it is also true that you can't construct statements in : without a prior ? but .. its hardly a single operator in syntax terms if it has two d…
> its hardly a single operator in syntax terms if it has two disjoint components I don't think "operator in syntax terms" is nearly as well-defined as OP thinks. Why couldn't `?` be parsed as half an operator and `:` as the other half? There's no rule that says a parser has to call each distinct symbol token its own "operator". In fact, I'd argue that the only reason this might seem seem like a rule is that almost al…
Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.
Looking forward to read it during Summer time.
Minor thing. Purely as a side: in C and C++, the conditional statement is written using if and else, while the conditional expression is written with a ternary operator ? and :. ending a sentence with . is a must. Including a period directly after a syntactic construct about ? and : is .. jarring because it is possible to attempt to read this as :. as an atomic construct in the language. Or even worse, the three-dots…
I'm interested to know why I would want to learn Lean if I'm already familiar with Idris.
* tactics (proof scripts are a lot easier than manual proving)
* syntax extensibility (Racket-like, supports custom elaboration/delaboration)
* mathlib (library of formalized math)
* tooling (can't say it's better, I haven't used Idris, but it's at least a lot nicer than Agda's: rustup-like version manager `elan`, own build system `lake`, official vscode extension supporting mini web apps which can interact with the code)
Small things I can remember:
* do-notation with early return and imperative loops
* easier termination proof handling (provide some expression using function arguments with `decreasing_by` and prove it's decreasing with `termination_by` block, which may be automatic even for non-structural recursion because of some built-in tactic)
Is this production ready ? How about performance (comparison with Rust)
Tooling around it great (it is installed with a rustup fork called elan).
As far as performance, it uses a particular version of ref-counting that allows mutation of unique references based on run-time tracking rather than compile time. If you accidentally keep a reference to an array and modify it, then you end up copying it rather than just mutating it.