To me as a programmer, to write mathematical proofs that are mechanically checked by a computer feels empowering. To have these proofs as executable programs feels even more empowering. Therefore, our proofs have a computational aspect and vice-versa: our programs have a logical aspect. To be able to get an instant feedback while proving a theorem is amazing. With Agda, a dependently typed functional programming language, one can interactively write a proof by getting guidance from Agda as to what is left to prove. Furthermore, Agda checks the correctness of proofs by following a set of rules. Unlike with pen and paper proofs, proofs in Agda are much more rigorous because there is no room for hand-waving nor unwarranted claims for something to be trivial. An uninformed mathematician will likely find this comparison to Agda hard to believe.

# Category Archives: functional programming

# Gave a Talk: Terminating and Productive Functions

At the Lambda Zagreb Meetup this Monday I gave a talk on terminating and productive functions. It was an interesting discussion with questions that tied the topic and examples I had with natural numbers, linear types and communicating systems.

## Giving Talk on Productive and Terminating Functions

### Status

Today I’ll be giving a talk on terminating and productive functions as part of the Lambda Zagreb Meetup group. This talk will be very familiar to my upcoming Lambda Days 2019 talk.

## Speaking at Lambda Days 2019!

### Status

I’m happy to announce that I’ll be speaking at the Lambda Days 2019 conference! I’ll be giving a talk on function totality.

# Programming Lego Mindstorms EV3 in Haskell

Earlier this week I got a Lego Mindstorms EV3 robotics kit. I was aware there is a Haskell binding, but I didn’t know it is compatible only with the earlier NXT generation of the Mindstorms line, at least according to the Wikipedia page on EV3. I’m hoping to find out today if the NXT Haskell library can nevertheless be used with the EV3. If not, I’m likely to start writing a Haskell library for EV3.

# Gave a Talk on Function Totality

As announced last week, yesterday I gave a talk on function totality at the Institute of Electrical and Electronics Engineers, Croatian Section. The talk was located at the University of Zagreb at the Faculty of Electrical Engineering and Computing. Slides used during the talk are freely available. The talk was in Croatian.

## Giving a Talk at IEEE on Function Totality

### Status

The upcoming Tuesday I will be giving a talk at the IEEE Croatian Section on function totality. The talk will take place at the University of Zagreb, the Faculty of Electrical Engineering and Computing.

# Function Totality: Abstraction Tool in Programming

Edsger Dijkstra said the following of abstraction:

“The purpose of abstraction is not to be vague, but to create a new semantic level in which one can be absolutely precise.”

Abstraction is a cornerstone of programming a complex software system. Without it, a complex software system is a complicated software system. In this article I will explore an important tool in achieving abstraction in programming: function totality.

## Proof Assistant in Teaching

### Status

Benjamin C. Pierce writes what it is like to use a proof assistant to teach programming language foundations.

# Hooked on Dependent Types

Just this morning these two books landed my mailbox:

The Little Typer is a new book on dependent type theory, written by Daniel P. Friedman, an author of The Little Schemer, and David Thrane Christiansen, an Idris contributor. Verified Functional Programming in Agda is a book by Aaron Stump, on using dependent types in Agda to prove various properties of programs. After having read the Type-driven Development with Idris book by Edwin Brady, I am hoping these two books will significantly expand my knowledge of and improve my skills in type theory, theorem proving and typed functional programming. Looking forward to reading the books! If you haven’t noticed by now, I got hooked on dependent types!