by Mark Gritter | at Minnebar 16 | 3:45 – 4:30 in Proverb-Edison | View Schedule
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 is a Founding Engineer at Akita Software, his fourth startup experience, building API observability. Mark formerly worked 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.
