Weekly Review - Week 12

This post is a summary of my activities related to coding and software in the past week. Its purpose is both to serve as a high-level personal log and as a potential source of interesting (or not so interesting) links. Entries are provided in no particular order with minimal comments…

Grammatical Framework

A fascinating piece of work whose purpose is to provide a way to define unified grammars that can be “linearized” into different languages for the purpose of both parsing and text generation.

Emacs Daemon on Mac OS X

Configuration for running Emacs in server mode which is useful for fast editing of files from the command-line: Run emacsclient foo.txt& and the file’s content is displayed in a buffer in emacs.

La lutte pour la reconnaissance

Finished reading this book from Axel Honneth, a German philosopher heir to the Frankfurt School. Worthy of some extended blog post…

Capture org-mode links in Firefox

A nice utility to quickly capture links in Firefox and add them to Emacs’ org-mode

Huggin

A tool in Rails to create and manage agents on a personal server, something I have been thinking to setup for a while.

Syncthing

Open-source system to synchronize several devices

Types + Properties = Software - Mark Seemann on Vimeo

While working on my talk for Crafting Software meetup, I discovered previous work from Mark Seeman in the same vein. There is a whole blog post series on Types + Properties = Software which is definitely interesting. Inspired The Polyglot Approach to Getting Better at Modeling the State and Writing Property Tests in Elm · Exceptional Mirrors written in Elm.

Reverse, Reverse: Theorem Proving with Idris

A blog post on how theorem proving works in Elm, detailing the classical vector reversal function’s derivation.

idris-tutorial.pdf

A short tutorial on Idris by Edwin Brady. Not sure how relevant it is to the newest versions of the language, but provides a compact overview of Idris’ features.

Agda Tutorial

Working on Idris led me to Agda which is a predecessor of Idris with an emphasis on theorem proving.

How can I express range validity in Idris?

As I was struggling on writing some Idris code for my talk, I posted this question on SO which leads to a Ah!Ah! moment thanks to the answer it received: The slogan is Add more information to your types!

Type Theory and Functional Programming

An out-of-print book by Simon Thompson (author of one of the first Haskell books) that seems to provide a lot of insights on top of Pierce’s classical textbook.

Brutal {Meta}Introduction to Dependent Types in Agda

A page full of resources on dependent types, not only in Agda. Lead me to this post from Lennart Augustsson which gives an implementation of a depedently-typed lambda calculus in Haskell.

Wardley Maps

I have started again to read Simon Wardley’s book-in-progress on how to draw maps for strategic thinking.