Disgruntled Code

Computers / Math / Stuff

Back to Basics

Refreshing Restarts

So I have finally broken down. I can’t do it any longer. I’m getting sick of the web, and all of its “responsive” designs and distracting “polish”. It has its place, perhaps, but its place is not with me.

This website never sat quite right with me. It was too… Bootstrappy. It was never really my own, and I suppose that’s part of why I never felt much like updating it. It wasn’t me, and frankly I was somewhat embarrassed by the half-baked attempt at the web 3.0s.

No longer! I’d rather have no CSS than crappy CSS, and thus here we are. With damn near no CSS, and essentially a blank HTML document with tiny bits of bedazzlement. Somehow it feels more like home.

Read more / comment »

No Bug November, WILTW


Hoof! Lots of papers, lots of writing!

Taking a peek into the Firefox verified crypto, and a bunch of Coq libraries and frameworks.

Read more / comment »

What I Learned This Week: Tapir


This week has largely been administrative, with letters written, and servers managed.

I went through the Tapir/LLVM paper, and had some thoughts about theorem proving…

Read more / comment »

What I Learned This Week: Subset types, real numbers, and more Coq


This has been a productive week with my Coqplexity project really starting to get off of the ground. Coqplexity is at the point now where it can automatically prove pretty much any polynomial Big O relation (as long as it’s true).

Some more work needs to be done in Coqplexity in order to make it more useful, but the foundation is there, and it’s been a good bit of experience in writing tactics and dealing with real numbers.

So, more stuff about subset types, tactics, and more!

Read more / comment »

What I Learned This Week: Real Numbers in Coq


This week more or less concludes my search for a real number library in Coq, allowing me to get another project underway which needed real numbers!

Additionally I have been messing a little bit more with subset types, which should prove useful in the very near future.

Read more / comment »

What I Learned This Week: Progress Sensitive Security, Erasure


Let’s keep this going! The goal of this is again, to write down some of my thoughts and what I did. This is not necessarily going to be accurate, but maybe it will be useful! Contact me if you find mistakes :).

The past week I have managed to get through another chunk of papers on the following topics:

  • Removing information leaks through the progress covert channel
  • Ensuring data erasure in programs which use untrusted data stores

Additionally, I have started to research real number libraries in Coq for use in a project…

Read more / comment »

What I Learned This Week: Coinduction, Dependent Pattern Matching, and Langsec


I’m starting a small series. The gist of it? What I learned in the past week.

Each post will be a brief summary of some things which I studied in the past week. Not necessarily an in depth exploration of the topics, but you may find useful insight, or at least useful references if something is a topic of interest.

If you find a mistake in my understanding, or have a question, feel free to contact me!

With that out of the way, let’s talk about some of the things I read about this week. Coinduction in Coq, dependent pattern matching in Coq, and some papers in langsec.

Read more / comment »

A Journey Through Types

I’m giving a talk as an introduction to dependently typed programming languages. The contents of this talk can be found in this post, and the slides can be found here.

Read more / comment »

Arm on Haskell

I wrote a post about setting up Haskell development for ARM over on the Haskell Embedded blog that I’m a part of. You should check it out!


Read more / comment »

Absolutely Optimal

Program optimization is strange.

We naturally want our programs to run as quickly and efficiently as possible, but in some sense I have no idea what that actually means. Or, rather, I have no idea what “computation” actually entails.

Read more / comment »

First Post!


I now apparently have a blog. I don’t know if this will ever see an update, or if this will ever be read by anybody, but the intention is to put some ramblings up here.

Read more / comment »