Oblique Note on Methodologies

In all optimization problems the solutions must incorporate the biases of the objective function otherwise they are sub-optimal solutions and will be beaten by solutions that exploit more of the structure/biases inherent in the objective function. Evolution works iteratively on short timescales and as byproducts/solutions of the evolutionary objective function we incorporate the short term biases/structures inherent in evolution. I think this means long term thinking and planning is fundamentally a doomed enterprise for organisms like us and if you want to be rich and famous then appeal to the here and now.

This is why I no longer think agile is a good way to develop software. It’s impossible to do any kind of longer term planning and work with an agile methodology. More specifically, any kind of long term thinking will not survive in an agile environment because it won’t exploit the planning structures inherent in the agile process.

Variation of the Pigeonhole Principle

In math, the pigeonhole principle states that if n items are put in m containers and n is greater than m then at least two items must go in the same container. This principle is formalized in “Software Foundations” as follows

Theorem pigeonhole_principle : forall {X:Type} (l1 l2:list X),
  excluded_middle ->
  (forall x, In x l1 -> In x l2) ->
  length l2 < length l1 ->
  repeats l1.
Continue reading

Preliminary Impressions of Software Foundations

This post is mostly an excuse for me to understand solutions to some problems that I thought were hard. I’ll try to structure things in a way so that if you still want to solve the problems yourself then you can just read enough for a hint and then try some things with the hint in mind. There is no shame in looking at the solutions because I had to look myself. The informal proofs were easy but convincing Coq of the informal reasoning was beyond me so I looked up the solutions.

The problems come from the chapter on inductive propositions. The chapter itself is a bit unevenly paced so don’t fret if you have trouble with it.

Continue reading

Formal Methods Will Never Be Mainstream

No matter how much I wish for formal methods to become more mainstream I’m going on the record to say that they’ll never be mainstream. It’s too much for the typical software engineer. The gap between what regular software engineering looks like and what formal methods look like is just too wide and I don’t think there is any simple or even complicated way to close that gap. There is an irreducible amount of complexity when it to comes to stating and proving theorems and the only system up to the task is the human brain. So far the neural net people haven’t figured out how symbolic reasoning works and formal methods are the domain of symbolic methods.

Continue reading

What Exactly is Composable?

Programmers tend to throw this word around a lot but it’s often not clear what it means. At the lowest level we have syntax, grammar, and source code. At this level almost everything is composable. Moving up a few levels we get to semantics and semantic composition and this is where things get a bit more tricky. This is the level where most of the discussions tend to happen. I’m going to use threads as an example to demonstrate the point. The code snippets will be in Ruby.

Continue reading

Existential Quantification in Type Theory

All of logic can be encoded with a suitable type theory and this includes the usual existential and universal quantifiers. The universal quantifier is easy because it corresponds to Π types but the existential quantifier is a little more tricky. It took me some time to make sense of it so here’s a small outline of how to think about it (this is as much to help me understand as it is for someone else so if you find any issues then let me know).

Continue reading

The Cost of Bad Software Architecture

Let me know if this sounds familiar. You work at a software company that uses a 3/3.5 tier architecture. There are frontend servers, backend servers, some batch work servers, and a database or two. If it doesn’t sound familiar then maybe you have never worked with web application but that’s the predominant architecture at most web shops. In fact, even with all the microservice/devops/container/serverless hype no one has managed to change that 3/3.5 tier architecture. There is always a frontend, there is always a backend, there is always a database. The only differences are in the domain logic and implementation details like which language is used for the backend components and which database is used to hold the data. Let’s now get into some more concrete but still abstract details because I promise there is point at the end of this.

Continue reading

Involutions are Bijections

I’m starting to get more of the pieces of the theorem proving puzzle. Going through “Software Foundations” and having “Type Theory and Formal Proof” as a reference has been very helpful with putting the pieces together. I’m starting to understand why folks like type theory. The encoding of logic and computation with types is surprisingly elegant. Most of the pieces fall out of abstraction and application/beta-reduction which is kinda amazing.

But enough of that. While going through “Software Foundations” I had to do an exercise about reversing lists. More specifically, reversing lists is an involution and involutions more generally are bijections so I wanted to prove this in the more general setting without having to worry about reversing lists.

Continue reading

Some Propositional Logic in Coq

I’ve been told the best way to learn is to do so let’s do some propositional logic with Coq. I got these exercises from the first two sessions of “The Incredible Proof Machine“.

I’m not sure how to translate contexts in sequent calculus other than making everything above the bar an input and everything below the bar an output so some of the exercises did not have analogs (like flipping the order of the premises). I either skipped those or made a best effort translation.

Continue reading