If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!
Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.
Building robust software is a hard task these days. As software gets more complex it gets increasingly hard to reason about it, this leads to a larger attack surface for bugs and security flaws.
Some of these bugs can be completely eliminated with the introduction of type systems that keep our values at runtime in check. Type systems are in fact the most widespread mechanism to verify correctness properties of programs, with dependent types we take this to the next level.
In this talk I will introduce techniques for programming with dependent types as well as interaction with the programming language itself. Examples will present resource tracking in the type system e.g. tracking file handles and yielding compilation errors on resource leaks, modeling specifications of protocols as types and enforcing them.