F*: A general-purpose proof-oriented programming language

I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.