Learning about Lean, a language that's also a proof assistant.
I remember Edinburgh Uni lecturers (ML was born there) describing a language where you could include proofs alongside code, but the compiler ignored them.
30 years later, Lean can verify them.
I remember Edinburgh Uni lecturers (ML was born there) describing a language where you could include proofs alongside code, but the compiler ignored them.
30 years later, Lean can verify them.
