WARNING
Note on FFI Interface Stability The current Foreign Function Interface (FFI) in Lean 4 was primarily designed for internal use within the Lean compiler and runtime. As such, it should be considered unstable. The interface may undergo significant changes, refinements, and extensions in future versions of Lean. Developers using the FFI should be prepared for potential breaking changes and should closely follow Lean's development and release notes for updates on the FFI system.
Eric Taucher EricGT
ydewit
/ lean-ffi-article.md
Last active
October 30, 2025 21:50
Understanding Lean's Foreign Function Interface (FFI)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Classes | |
| * Keith Devlin - Introduction to Mathematical Thinking - https://www.coursera.org/learn/mathematical-thinking | |
| * Michael Genesereth - Introduction to Logic - https://www.coursera.org/learn/logic-introduction | |
| * Robert Harper - Homotopy Type Theory - http://www.cs.cmu.edu/~rwh/courses/hott/ | |
| Books and Articles | |
| * Benjamin C. Pierce - Types and Programming Languages - https://www.cis.upenn.edu/~bcpierce/tapl/ | |
| * x775 - Introduction to Datalog - https://x775.net/2019/03/18/Introduction-to-Datalog.html | |
| * Bartosz Milewski - Category Theory For Programmers - https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ | |
| * Benjamin C. Pierce et al. - Software Foundations - https://softwarefoundations.cis.upenn.edu/ |