writing on programming etc by daniel patterson
How to prove a compiler fully abstract by Daniel Patterson on April 19, 2018 A compiler that preserves and reflects equivalences is called a fully abstract compiler. This is a powerful property for a compiler that is different (but complimentary) to the more common notion of compiler correctness . So what does it mean, and how do we prove it? All the code for this post, along with instructions to…
How to prove a compiler correct by Daniel Patterson on January 16, 2018 At POPL’18 (Principles of Programming Languages) last week, I ended up talking to Annie Cherkaev about her really cool DSL (domain specific language) SweetPea (which she presented at Off the Beaten Track 18, a workshop colocated with POPL), which is a “SAT-Sampler aided language for experimental design, targeted for Psychology…
(Cheap) home backups by Daniel Patterson on January 1, 2018 Backing things up is important. Some stuff, like code that lives in repositories, may naturally end up in many places, so it perhaps is less important to explicitly back up. Other files, like photos, or personal documents, generally don’t have a natural redundant home, so they need some backup story, and relying on various online services…
Why test in Haskell? by Daniel Patterson on October 5, 2014 Every so often, the question comes up, should you test in Haskell, and if so, how should you do it? Most people agree that you should test pure, especially complicated, algorithmic code. Quickcheck 1 is a great way to do this, and most Haskellers have internalized this (Quickcheck was invented here, so it must provide value!). What’s less…
A Hacker's Replacement for GMail by Daniel Patterson on June 29, 2013 Note: Since writing this I’ve replaced Exim with Postfix and Courier with Dovecot. This is outlined in the Addendum, but the main text is unchanged. Please read the whole guide before starting, as you can skip some of the steps and go straight to the final system. Motivation I reluctantly switched to GMail about six months ago,…
A Literate Ur/Web Adventure by Daniel Patterson on May 21, 2013 Ur/Web is a language / framework for web programming that both makes it really hard to write code with bugs / vulnerabilities and also makes it really easy to write reactive, client-side code, all from a single, simple, codebase. But it is built on some pretty deep type theory, and while it is an incredibly practical research project,…
Programming as Literature by Daniel Patterson on October 24, 2012 Sometimes I’m not sure how to explain what I study or why I study it. I tell people that I study theoretical computer science, or algorithms and programming languages, or math and computer science, and if they ask why? Let’s come back to that. First I want to talk about literacy. Literacy is about being able to understand the…
Haskell / Snap ecosystem is as productive as Ruby/Rails. by Daniel Patterson on April 26, 2012 This may be controversial, and all of the usual disclaimers apply - this is based on my own experience using both of the languages/frameworks to do real work on real projects. Your mileage may vary. Because this is something that has the potential to spiral into vague comparisons, I am going to try to…
Math/Science integrated with Scheme by Daniel Patterson on December 6, 2011 I had an idea today, of an interactive homework assignment for a Chemistry class. It was a prompt, and you could type in queries and it would give responses. The basics would be: # (questions) => To Do: (1,2,3,4,5,6,7) Complete: () # (question-1) => 1. How many grams of Na are needed to make 28 grams of NaCl? #…
iOS is anti-UNIX and anti-programmer. by Daniel Patterson on September 15, 2011 When I was first learning about UNIX, and learning to use Linux, the most immediately powerful tool that I found was the shell’s pipe operator, ‘|’. Using the commandline (because at that point, linux GUI’s were not so well developed, and the few distros that tried to allow strictly graphical operation usually failed…