lean is pretty sweet

Stream: general

[Andrew Ashworth]

i went back to doing some programming in fsharp since its the only mixed-paradigm language with any traction, and i really miss lean

[Andrew Ashworth]

doing everything in the equivalent of meta def land is no fun

[Simon Hudon]

What do you miss about trusted code?

[Andrew Ashworth]

i like when the compiler spots issues for me and not runtime exceptions

[Andrew Ashworth]

on the other hand being able to call into a bajillion .NET libraries is also pretty awesome... sigh

[Simon Hudon]

I'm wondering if the type vs untyped languages will gain one dimension:

• (Haskell / F# proponent to JavaScript programmers): why does your language not have types? Come over to the civilized world!
• (Lean user to Haskell / F# programmer): why can't you write proofs in your language? Come over to the civilized world!

[Scott Morrison]

Let's hope so. :-)

[Simon Hudon]

on the other hand being able to call into a bajillion .NET libraries is also pretty awesome... sigh

True but doesn't it scare you how weak their contracts are? Does this function terminate? Does it perform io? Does it mutate state? Does it satisfy beautiful laws? Who knows! It's just a chunk of code that does stuff

[Andrew Ashworth]

the important thing is that it's a chunk of code i didn't write

[Andrew Ashworth]

i mean, i write all my quick and dirty scripts in python for that reason

[Mario Carneiro]

For me it's more than just being able to write proofs. I think a better characterization is the ability to have really expressive types, like a type of prime numbers, or expressing pre/post-conditions of a function in the type

[Simon Hudon]

That is pretty cool, true

[Simon Hudon]

I especially like that type classes come with laws

[Andrew Ashworth]

i hope the ffi story is good in lean 4, then you could use lean for more than just standalone projects

[Mario Carneiro]

and of course, being able to substantively make use of a nontrivial precondition, like if you have a list and a proof it is [] then you don't even have to supply the cons case

[Mario Carneiro]

and there are no apologetics or assertions or unreachables

[Andrew Ashworth]

too bad lean can't bootstrap lean

[Simon Hudon]

What do you mean by no assertions?

[Simon Hudon]

Do you mean that the assertions are not checked dynamically?

[Mario Carneiro]

In any other programming language, if I have a division function with a precondition, I still have to handle the case when the precondition is violated, and maybe throw an assertion violation or unreachable exception. The compiler can't prove that you are following your precondition so it has to be done

[Mario Carneiro]

but in lean I can just omit the case and it can prove that the branch is impossible, so it's just not a code path

[Simon Hudon]

Darn! You're right! I really don't miss that! Especially the Java flavor. Luckily, I haven't touched Java in years

[Andrew Ashworth]

if you're on the JVM, scala isn't bad

[Andrew Ashworth]

haven't had a chance to use it very much though

[Andrew Ashworth]

but i know people who speak highly of it

[Scott Morrison]

I've written a lot of Scala, and in particular a lot of maths in Scala. I'm hoping to never go back, however. :-)

[Scott Morrison]

(It is great, but Lean is greater still.)

[VinothKumar Raman]

I've written a lot of Scala, and in particular a lot of maths in Scala. I'm hoping to never go back, however. :-)

I was trying to do something like this in scala, https://scalafiddle.io/sf/enaGqD4/0 I hated myself why I thought it might work, and original version, without defining natural induction is this https://scalafiddle.io/sf/A56KTgD/1 (I made lot of changes its not compiling, I dont remember now what I did and its completely incomprehensible now)

[Mario Carneiro]

This reminds me of those people that wrote a BF interpreter in C++ template language

[VinothKumar Raman]

Yea, it felt more like programming in BF itself. But I understand a lot about types now after the ordeal.