diff --git a/README.md b/README.md index 938dd46..57e9109 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,13 @@ # TypeTalk -Calvin Talks Types + +A talk about the wonderful world of types and programming languages, +with a dash of formal verification. Does your programming language get +you down? It probably should! Ever wish you could prove that your +program was correct? Maybe you can! Join us as we briefly explore some +alternatives with typed functional programming languages. With a bit +of luck you will catch a glimpse into how programming languages can +make your lives easier, and the world a better and safer place. Types +aren't the Java-esk horrors of your nightmares, instead they can make +programming a pure delight! Let's discover why that annoying person +keeps talking about Haskell, and why that even more obnoxious person +won't shut up about Idris. diff --git a/presentation/presentation.pdf b/presentation/presentation.pdf index ba1c6c0..5a1605e 100644 Binary files a/presentation/presentation.pdf and b/presentation/presentation.pdf differ diff --git a/presentation/presentation.tex b/presentation/presentation.tex index 25d3d39..77d466a 100644 --- a/presentation/presentation.tex +++ b/presentation/presentation.tex @@ -51,8 +51,16 @@ \section{Introduction} Types! This presentation hopes to address the following: \begin{itemize} - \item How types make things easier to write. \item How types can help you write correct software. + \begin{itemize} + \item This is important when \emph{EVERYTHING} runs software. + \item Good type systems can make this less horrifying! + \end{itemize} + \item How types make things easier to write in general. + \begin{itemize} + \item Compiler can automate a lot more. + \item Compiler can catch many simple issues. + \end{itemize} \end{itemize} \pause @@ -206,11 +214,11 @@ \section{The types you may have seen} \begin{itemize} \pause + \item Very verbose. Lots of additional syntactic cruft. + \pause \item Can see what functions accept and return! \pause \item Null references... :c - \pause - \item Very verbose. Lots of additional syntactic cruft. \end{itemize} \pause @@ -237,6 +245,12 @@ \section{The types you may have seen} \item Stop us from making mistakes. \end{itemize} \pause + \item Allow us to make better guarantees. + \begin{itemize} + \item ``Function does not alter global state'' + \item ``Function does not read from disk'' + \end{itemize} + \pause \item Not too much verbosity. \begin{itemize} \item Nice, clean syntax! @@ -248,6 +262,7 @@ \section{Haskell} \begin{frame}[fragile] \frametitle{Introducing Haskell!} + \pause \begin{lstlisting}[frame=single, language=Java, breaklines=true, basicstyle=\ttfamily\tiny] def my_sort(xs): if xs == []: diff --git a/talk.org b/talk.org index 7a9ae9f..d61a714 100644 --- a/talk.org +++ b/talk.org @@ -4,35 +4,37 @@ Hi all! My name is Calvin and I'm here to talk to you about a couple of things --- mostly types, and how they can help you write correct programs! I -have a couple bullet points to summarize what I want to talk -about: +-- mostly types, and how they can help you write correct programs! +This talk aims to address some of the following: -1) You should care, and you NEED to care about your software. - Computers are integral to *every* aspect of our lives, an their - influence grows daily. Whether it's a voting machine, banking - software, or a component of a vehicle, there's always a programmer - behind it somewhere. - This should terrify you if you have ever programmed before. +1) Firstly: + You should care, and you NEED to care about your software. + Computers are integral to nearly *every* aspect of our lives, and + their influence is growing daily. Whether it's a voting machine, + banking software, or a component of a vehicle, there's always a + programmer behind it somewhere. - An incorrect program may just be annoying and lose a business a - customer, or an incorrect program could kill somebody if it's - something vital, like software running a pacemaker. + And this fact should probably terrify you if you have ever + programmed before. - We need to be careful! + An incorrect program may be annoying and lose a business a + customer, or it could be life threatening if it's something vital, + like the software for a pacemaker. -2) Types are a good way to help you with how scary the first point is! + We need to be careful! + + Types can help us be careful, and are a good way to deal with how + scary this is! -3) Not only are types great for writing correct programs, but they can - make it a lot easier to write programs in the first place! They help - the compiler help you! +2) Secondly, not only are types great for writing correct programs, but they can + make it a lot easier to write programs in the first place! They + help the compiler help you! This is going to be somewhat of a whirlwind introduction to the world of types, so if you get lost along the way that's okay. Just let me -know and hopefully I can clarify things along the way, and if I can't -do that in the allotted time, don't fret! Talk to me after the fact! -Sometimes it takes a while to grok mathy stuff! +know and hopefully I can clarify things. If all else fails talk to me +after the fact! Sometimes it takes a while to grok mathy stuff! * What are we trying to solve? @@ -42,11 +44,14 @@ You think that this is a normal, and necessary thing: That's bad. Runtime exceptions don't actually /have/ to exist, and it can be very bad if our pacemaker segfaults. So maybe we should avoid -these problems in the first place! I'll talk a bit about what we can -do to avoid these problems. Later on in the talk we'll dip a little -into how you can guarantee that the logic in your program is correct -too, and not just that it does not explode at runtime. All of this is -going to involve a little help from types. +these problems in the first place! + +I'll talk a bit about what we can do to avoid these problems. Later +we'll look a little into how you can guarantee that the logic in your +program is correct too, and not just that it does not explode at +runtime. + +All of this is going to involve a little help from types. * What is a type? @@ -113,11 +118,13 @@ going to involve a little help from types. really damn hard. In a large code base it's difficult to even know what you should - pass to a function. Should it take a list, or a set? Should it take - an int, or a float? This factorial function only works with ints (a - non-integer number will never trigger the base case), but you might - not realize you're calling it with floats until it's too late! Can - you simply pass the result of another function to this one, or + pass to a function. Should it take a list, or a set, or an integer? + + This factorial function only works with ints (a non-integer number + will never trigger the base case), but you might not realize you're + calling it with floats until it's too late! + + Can you simply pass the result of another function to this one, or might that function return None, which this factorial function can't handle? You can't know for sure until you read what that other function does, and what every function that function calls