Functions are Proofs: an Introduction to the F* Language
by Mark Gritter | at Minnebar 16
When you're writing a computer program, you're telling the computer what to do. But what if you could also tell it what your code should do?
Many programming languages have types. A compiler (or type-checker) can verify that those types are correct. But what if you could create new types the compiler could check for you? Things like "a list that contains elements in ascending order" or "this graph contains no cycles" or even "this integer is the minimum element of a particular list"!
F* is a "proof-oriented programming language" similar to OCaml, created by Microsoft Research. It has "dependent types", which give the flexibility to describe constraints like those above, and uses a SMT solver back-end to help you verify properties about your programs. F* programs will be proofs of correctness--- but they will still be working code! The F* language has been used in practice for verified cryptographic primitives and robust parsers. I'll explain how the language works, show some examples, and demonstrate how to put the Curry-Howard Isomorphism to work for you!
Mark Gritter
Mark Gritter is a Founding Engineer at ThirdLaw, his fifth startup experience, building monitoring and control for AI systems.
Mark formerly worked at Akita Software and Postman on API observailbity; at HashiCorp on the Vault team; co-founded Tintri, an enterprise storage company that IPOed in 2017; and was a day-one employee at Kealia, a video streaming startup acquired by Sun Microsystems in 2004.
Mark's previous Minnebar presentations have covered topics such as correctness of algorithms, combinatorial auctions, scaling a startup, building a file system, and procedural content generation.
Links: