Thursday, July 06, 2017

HaskellX Bytes talk next Tuesday

I'm talking about "Static Analysis in Haskell" at HaskellX Bytes next Tuesday (11th July), in London UK. Registration is free. The abstract is:

Haskell is a strongly typed programming language, which should be well suited to static analysis - specifically any insights about the program which don't require running the program. Alas, while type systems are becoming increasingly powerful, other forms of static analysis aren't advancing as fast. In this talk we'll give an overview of some of the forms of non-type-based static analysis that do exist, from the practical (GHC warnings, HLint, Weeder) to the research (LiquidHaskell, Catch).

I'm a big fan of static analysis, so this will be part summary, part sales pitch, and part call to arms. Followed by beer.

Clarification: I originally got the day wrong, and the url persists the original incorrect day. The talk is on Tuesday 11th July.

Tuesday, June 20, 2017

Announcing Weeder: dead export detection

Most projects accumulate code over time. To combat that, I've written Weeder which detects unused Haskell exports, allowing dead code to be removed (pulling up the weeds). When used in conjunction with GHC -fwarn-unused-binds -fwarn-unused-imports and HLint it will enable deleting unused definitions, imports and extensions.

Weeder piggy-backs off files generated by stack, so first obtain stack, then:

  • Install weeder by running stack install weeder --resolver=nightly.
  • Ensure your project has a stack.yaml file. If you don't normally build with stack then run stack init to generate one.
  • Run weeder . --build, which builds your project with stack and reports any weeds.

What does Weeder detect?

Weeder detects a bunch of weeds, including:

  • You export a function helper from module Foo.Bar, but nothing else in your package uses helper, and Foo.Bar is not an exposed-module. Therefore, the export of helper is a weed. Note that helper itself may or may not be a weed - once it is no longer exported -fwarn-unused-binds will tell you if it is entirely redundant.
  • Your package depends on another package but doesn't use anything from it - the dependency should usually be deleted. This functionality is quite like packunused, but implemented quite differently.
  • Your package has entries in the other-modules field that are either unused (and thus should be deleted), or are missing (and thus should be added). The stack tool warns about the latter already.
  • A source file is used between two different sections in a .cabal file - e.g. in both the library and the executable. Usually it's better to arrange for the executable to depend on the library, but sometimes that would unnecessarily pollute the interface. Useful to be aware of, and sometimes worth fixing, but not always.
  • A file has not been compiled despite being mentioned in the .cabal file. This situation can be because the file is unused, or the stack compilation was incomplete. I recommend compiling both benchmarks and tests to avoid this warning where possible - running weeder . --build will use a suitable command line.

Beware of conditional compilation (e.g. CPP and the Cabal flag mechanism), as these may mean that something is currently a weed, but in different configurations it is not.

I recommend fixing the warnings relating to other-modules and files not being compiled first, as these may cause other warnings to disappear.

Ignoring weeds

If you want your package to be detected as "weed free", but it has some weeds you know about but don't consider important, you can add a .weeder.yaml file adjacent to the stack.yaml with a list of exclusions. To generate an initial list of exclusions run weeder . --yaml > .weeder.yaml.

You may wish to generalise/simplify the .weeder.yaml by removing anything above or below the interesting part. As an example of the .weeder.yaml file from ghcid:

- message: Module reused between components
- message:
  - name: Weeds exported
  - identifier: withWaiterPoll

This configuration declares that I am not interested in the message about modules being reused between components (that's the way ghcid works, and I am aware of it). It also says that I am not concerned about withWaiterPoll being a weed - it's a simplified method of file change detection I use for debugging, so even though it's dead now, I sometimes do switch to it.

Running with Continuous Integration

Before running Weeder on your continuous integration (CI) server, you should first ensure there are no existing weeds. One way to achieve that is to ignore existing hints by running weeder . --yaml > .weeder.yaml and checking in the resulting .weeder.yaml.

On the CI you should then run weeder . (or weeder . --build to compile as well). To avoid the cost of compilation you may wish to fetch the latest Weeder binary release. For certain CI environments there are helper scripts to do that.

Travis: Execute the following command:

curl -sL | sh -s .

The arguments after -s are passed to weeder, so modify the final . if you want other arguments.

Appveyor: Add the following statement to .appveyor.yml:

- ps: Invoke-Command ([Scriptblock]::Create((Invoke-WebRequest '').Content)) -ArgumentList @('.')

The arguments inside @() are passed to weeder, so add new arguments surrounded by ', space separated - e.g. @('.' '--build').

What about Cabal users?

Weeder requires the textual .hi file for each source file in the project. Stack generates that already, so it was easy to integrate in to. There's no reason that information couldn't be extracted by either passing flags to Cabal, or converting the .hi files afterwards. I welcome patches to do that integration.

Sunday, June 11, 2017

Haskell Website Working Group - Update

Summary: We have agreed a set of principles for the website and are collecting information.

I'm writing this partly in my capacity as the chair of the Haskell Website Working Group, and partly as an individual (so blame me rather than the committee). It's fair to say that the original goal of the committee was to make sure everyone agrees on the download page. Discussions amongst the committee lead to a shared goal that the download page itself should clearly direct users along a precise path, without requiring beginners to make decisions requiring judgement. That probably means that download page should only describe one installation path, pushing alternatives onto a separate page.

To decide what should go on the download page, our first step was to evaluate what was currently available, and what experience a beginner might have. We've started that on this page. As an example, it says how to install Haskell, how to open ghci, how to install a tool etc - all using the different options.

When I actually tried installing and using the various options listed on the current download page, they all had confusing steps, unintuitive behaviour and problems that I had to overcome. As an example, Stack on Windows recommends using the 32bit version, while noting that only the 64bit version works. At the same time, Core Platform starts by telling me to edit a global Cabal config file.

I invite everyone to help contribute to that page, via pull requests. At the same time, it would be great if the issues raised could be ironed out, leading to a smooth beginner experience (I'm talking to maintainers in person and raising GitHub tickets). Once the information is collected, and ideally the tools have improved, it will be time to make a decision between the options. When the decision comes, it will be technically motivated, and hopefully unambiguous.

Sunday, May 21, 2017

Proving fib equivalence

Summary: Using Idris I proved the exponential and linear time fib functions are equivalent.

The Haskell wiki proclaims that Implementing the Fibonacci sequence is considered the "Hello, world!" of Haskell programming. It also provides multiple versions of fib - an exponential version and a linear version. We can translate these into Idris fairly easily:

fibExp : Nat -> Nat
fibExp Z = 0
fibExp (S Z) = 1
fibExp (S (S n)) = fibExp (S n) + fibExp n

fibLin' : Nat -> Nat -> Nat -> Nat
fibLin' Z a b = b
fibLin' (S n) a b = fibLin' n (a + b) a

fibLin : Nat -> Nat
fibLin n = fibLin' n 1 0

We've made the intermediate go function in fibLin top-level, named it fibLib' and untupled the accumulator - but it's still fundamentally the same. Now we've got the power of Idris, it would be nice to prove that fibExp and fibLin are equivalent. To do that, it's first useful to think about why fibLib' works at all. In essence we're decrementing the first argument, and making the next two arguments be fib of increasingly large values. If we think more carefully we can come up with the invariant:

fibLinInvariant : (d : Nat) -> (u : Nat) ->
    fibLin' d (fibExp (1+u)) (fibExp u) = fibExp (d+u)

Namely that at all recursive calls we must have the fib of two successive values (u and u+1), and after d additional loops we end up with fib (d+u). Actually proving this invariant isn't too hard:

fibLinInvariant Z u = Refl
fibLinInvariant (S d) u =
    rewrite fibLinInvariant d (S u) in
    rewrite plusSuccRightSucc d u in

Idris simplifies the base case away for us. For the recursive case we apply the induction hypothesis to leave us with:

fibExp (plus d (S u)) = fibExp (S (plus d u))

Ignoring the fibExp we just need to prove d+(u+1) = (d+u)+1. That statement is obviously true because + is associative, but in our particular case, we use plusSuccRightSucc which is the associative lemma where +1 is the special S constructor. After that, everything has been proven.

Armed with the fundamental correctness invariant for fibLib, we can prove the complete equivalence.

fibEq : (n : Nat) -> fibLin n = fibExp n
fibEq n =
    rewrite fibLinInvariant n 0 in
    rewrite plusZeroRightNeutral n in

We appeal to the invariant linking fibLin' and finExp, do some minor arithmetic manipulation (x+0 = x), and are done. Note that depending on exactly how you define the fibLinInvariant you require different arithmetic lemmas, e.g. if you write d+u or u+d. Idris is equipped with everything required.

I was rather impressed that proving fib equivalence wasn't all that complicated, and really just requires figuring out what fundamental property makes fibLin actually work. In many ways the proof makes things clearer.

Tuesday, May 16, 2017

Idris reverse proofs

Summary: I proved O(n) reverse is equivalent to O(n^2) reverse.

Following on from my previous post I left the goal of given two reverse implementations:

reverse1 : List a -> List a
reverse1 [] = []
reverse1 (x :: xs) = reverse1 xs ++ [x]

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []

Proving the following laws hold:

proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs

The complete proofs are available in my Idris github repo, and if you want to get the most out of the code, it's probably best to step through the types in Idris. In this post I'll talk through a few of the details.

Directly proving the reverse1 (reverse1 x) = x by induction is hard, since the function doesn't really follow so directly. Instead we need to define a helper lemma.

proof_reverse1_append : (xs : List a) -> (ys : List a) ->
    reverse1 (xs ++ ys) = reverse1 ys ++ reverse1 xs

Coming up with these helper lemmas is the magic of writing proofs - and is part intuition, part thinking about what might be useful and part thinking about what invariants are obeyed. With that lemma, you can prove by induction on the first argument (which is the obvious one to chose since ++ evaluates the first argument first). Proving the base case is trivial:

proof_reverse1_append [] ys =
    rewrite appendNilRightNeutral (reverse1 ys) in

The proof immediately reduces to reverse1 ys == reverse1 ys ++ [] and we can invoke the standard proof that if ++ has [] on the right we can ignore it. After applying that rewrite, we're straight back to Refl.

The :: is not really any harder, we immediately get to reverse1 ys ++ (reverse1 xs ++ [x]), but bracketed the wrong way round, so have to apply appendAssociative to rebracket so it fits the inductive lemma. The proof looks like:

proof_reverse1_append (x :: xs) ys =
    rewrite appendAssociative (reverse1 ys) (reverse1 xs) [x] in
    rewrite proof_reverse1_append xs ys in Refl

Once we have the proof of how to move reverse1 over ++ we use it inductively to prove the original lemma:

proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse1_reverse1 [] = Refl
proof_reverse1_reverse1 (x :: xs) =
    rewrite proof_reverse1_append (reverse1 xs) [x] in
    rewrite proof_reverse1_reverse1 xs in

For the remaining two proofs, I first decided to prove reverse1 x = reverse2 x and then prove the reverse2 (reverse2 x) = x in terms of that. To prove equivalence of the two functions I first needed information about the fundamental property that rev2 obeys:

proof_rev : (xs : List a) -> (ys : List a) ->
    rev2 xs ys = reverse2 ys ++ xs

Namely that the accumulator can be tacked on the end. The proof itself isn't very complicated, although it does require two calls to the inductive hypothesis (you basically expand out rev2 on both sides and show they are equivalent):

proof_rev xs [] = Refl
proof_rev xs (y :: ys) =
    rewrite proof_rev [y] ys in
    rewrite sym $ appendAssociative (rev2 [] ys) [y] xs in
    rewrite proof_rev (y :: xs) ys in

The only slight complexity is that I needed to apply sym to switch the way the appendAssocative proof is applied. With that proof available, proving equivalence isn't that hard:

proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
proof_reverse1_reverse2 [] = Refl
proof_reverse1_reverse2 (x :: xs) =
    rewrite proof_rev [x] xs in
    rewrite proof_reverse1_reverse2 xs in

In essence the proof_rev term shows that rev behaves like the O(n^2) reverse.

Finally, actually proving that reverse2 (reverse2 x) is true just involves replacing all the occurrences of reverse2 with reverse1, then applying the proof that the property holds for reverse1. Nothing complicated at all:

proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse2_reverse2 xs =
    rewrite sym $ proof_reverse1_reverse2 xs in
    rewrite sym $ proof_reverse1_reverse2 (reverse1 xs) in
    rewrite proof_reverse1_reverse1 xs in

If you've got this far and are still hungry for more proof exercises I recommend Exercises on Generalizing the Induction Hypothesis which I have now worked through (solutions if you want to cheat).

Sunday, May 07, 2017

Proving stuff with Idris

Summary: I've been learning Idris to play around with writing simple proofs. It seems pretty cool.

The Idris programming language is a lot like Haskell, but with quite a few cleanups (better export syntax, more though out type classes), and also dependent types. I'm not a massive fan of dependent types as commonly presented - I want to write my code so it's easy to prove, not intertwine my beautiful code with lots of invariants. To try out Idris I've been proving some lemmas about list functions. I'm very much an Idris beginner, but thought I would share what I've done so far, partly to teach, partly to remember, and party to get feedback/criticism about all the beginner mistakes I've made.

Before proving stuff, you need to write some definitions. Idris comes with an append function (named ++ as you might expect), but to keep everything simple and out in the open I've defined:

append : List a -> List a -> List a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

Coming from Haskell the only real difference is that cons is :: and types are :. Given how Haskell code now looks, that's probably the right way around anyway. We can load that code in the Idris interactive environment and run it:

$ idris Main.idr
Main> append [1,2] [3]
[1,2,3] : List Integer

What we can also do, but can't easily do in Haskell, is start proving lemmas about it. We'd like to prove that append xs [] = xs, so we write a proof:

proof_append_nil : (xs : List a) -> append xs [] = xs
proof_append_nil xs = ?todo

We name the proof proof_append_nil and then say that given xs (of type List a) we can prove that append xs [] = xs. That's pretty direct and simple. Now we have to write the proof - we first write out the definition leaving ?todo where we want the proof to go. Now we can load the proof in Idris and type :t todo to get the bit of the proof that is required, and Idris says:

todo : append xs [] = xs

That's fair - we haven't proven anything yet. Since we know the proof will proceed by splitting apart the xs we can rewrite as:

proof_append_nil [] = ?todo_nil
proof_append_nil (x :: xs) = ?todo_cons

We can now ask for the types of the two remaining todo bits:

todo_nil : [] = []
todo_cons : x :: append xs [] = x :: xs

The first todo_nil is obviously true since the things on either side of the equality match, so we can replace it with Refl. The second statement looks like the inductive case, so we want to apply proof_append_nil to it. We can do that with rewrite proof_append_nil xs, which expands to append xs [] = xs, and rewrites the left-hand-side of the proof to be more like the right. Refined, we end up with:

proof_append_nil [] = Refl
proof_append_nil (x :: xs) = rewrite proof_append_nil xs in ?todo_cons

Reloading again and asking for the type of todo_cons we get:

todo_cons : x :: xs = x :: xs

These things are equal, so we replace todo_cons with Refl to get a complete proof of:

proof_append_nil : (xs : List a) -> append xs [] = xs
proof_append_nil [] = Refl
proof_append_nil (x :: xs) = rewrite proof_append_nil xs in Refl

Totality Checking

Proofs are only proofs if you have code that terminates. In Idris, seemingly sprinkling the statement:

%default total

At the top of the file turns on the totality checker, which ensures the proof is really true. With the statement turned on I don't get any warnings about totality issues, so we have proved append really does have [] as a right-identity.

Avoiding rewrite

The rewrite keyword seems like a very big hammer, and in our case we know exactly where we want to apply the rewrite. Namely at the end. In this case we could have equally written:

cong (proof_append_nil xs)

Not sure which would be generally preferred style in the Idris world, but as the proofs get more complex using rewrite certainly seems easier.

Differences from Haskell

Coming from a Haskell background, and sticking to simple things, the main differences in Idris were that modules don't have export lists (yay), lists are :: and types are : (yay), functions can only use functions defined before them (sad, but I guess a restriction to make dependent types work) and case/lambda both use => instead of -> (meh).

Next steps

For my first task in Idris I also defined two reverse functions:

reverse1 : List a -> List a
reverse1 [] = []
reverse1 (x :: xs) = reverse1 xs `append` [x]

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []

The first reverse1 function is reverse in O(n^2), the second is reverse in O(n). I then tried to prove the three lemmas:

proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs

Namely that both reverse1 and reverse2 are self inverses, and then that they are equivalent. To prove these functions required a few helper lemmas, but only one additional Idris function/feature, namely:

sym : (left = right) -> right = left

A function which transforms a proof of equality from one way around to the other way around. I also required a bunch of helper lemmas, including:

proof_append_assoc : (xs : List a) -> (ys : List a) -> (zs : List a) -> append xs (append ys zs) = append (append xs ys) zs

Developing these proofs in Idris took me about ~2 hours, so were a nice introductory exercise (with the caveat that I've proven these lemmas before, although not in 4+ years). I'd invite anyone interested in learning this aspect of Idris to have a go, and I'll post my proofs sometime in the coming week.

Update: additional notes on this material can be found here from Reddit user chshersh.

Friday, April 28, 2017

HLint on Travis/Appveyor

Summary: Running HLint on your CI is now quick and easy.

I've always wanted to run HLint on my continuous integration servers (specifically Travis for Linux and Appveyor for Windows), to automatically detect code that could be improved. That has always been possible, and packages like lens and freer-effects have done so, but it was unpleasant for two reasons:

  • Setting up a custom HLint settings file and applying these settings was a lot of upfront work.
  • Building hlint on the CI server could be quite slow.

With HLint v2.0.4, both of these issues are addressed. I am now running HLint as standard for many of my projects. The two steps are outlined below.

Setting up custom HLint settings

Locally run hlint . --default > .hlint.yaml and it will generate a file which ignores all hints your project currently triggers. If you then run hlint . there will be no warnings, as the ignore settings will automatically be picked up. Check in .hlint.yaml.

Later, as a future step, you may wish to review your .hlint.yaml file and fix some of the warnings.

Running HLint on the server

There are now precompiled binaries at GitHub, along with scripts to download and execute them for each CI system. In both cases below, replace ARGUMENTS with your arguments to hlint, e.g. . to check the current directory.

On Travis, execute the following command:

wget -O - --quiet | sh -s ARGUMENTS

On Appveyor, add the following statements to .appveyor.yml:

- set PATH=C:\Program Files\Git\mingw64\bin;%PATH%
- curl -ohlint.bat -L

Since these are precompiled binaries the additional time required to run HLint should be minimal.

Thursday, April 06, 2017

HLint 2.0 - with YAML configuration

Summary: I've just released HLint 2.0, which lets you configure the rules with a YAML file.

I've just released HLint 2.0 to Hackage. HLint has always been configurable by writing a specially crafted Haskell file (e.g. to ignore certain hints or add new ones). With HLint 2.0 we now support YAML configuration files, and moreover encourage them over the Haskell format.

New Features of 2.0

Perhaps the most useful feature of this version is that HLint will search the current directory upwards for a .hlint.yaml file containing configuration settings. If a project includes a .hlint.yaml in the root then you won't need to pass it on the command line, and there's a reasonable chance any editor integration will pick it up as well. This idea was shamelessly stolen from Stylish Haskell.

HLint configuration files have also moved from Haskell syntax with special interpretation to YAML syntax. The Haskell syntax had become quite overloaded and was increasingly confused. The YAML syntax gives a fresh start with a chance to properly specify configuration directly rather than encoding it as Haskell expressions. The YAML configuration format enables a few features in this release, and going forward should enable more. To create a template .hlint.yaml file run hlint --default > .hlint.yaml. HLint continues to work without a configuration file.

In addition to a bunch of little hints, there is now a hint to suggest giving modules explicit export lists. I tend to always favour export lists, using module Foo(module Foo) where in the rare case they seem genuinely too much work. If you object to the hint, simply add to .hlint.yaml:

- ignore: {name: Use module export list}

On the other extreme, if you always want to require a complete and explicit export list (banning the trick above) do:

- warn: {name: Use explicit module export list}

Which enables the off-by-default hint requiring an explicit list. To see which off-by-default hints your program triggers pass the command line argument --show.

The biggest new hint is that you can now mark certain flags/extensions/imports/functions as being restricted - maintaining either a whitelist or blacklist and exceptions. As an example, HLint itself contains the restrictions:

- functions:
  - {name: unsafeInterleaveIO, within: Parallel}
  - {name: unsafePerformIO, within: [Util.exitMessageImpure, Test.Util.ref]}
  - {name: unsafeCoerce, within: []}

These unsafe functions can only be used in the modules/functions listed (or nowhere for unsafeCoerce), ensuring no code sneaks in unexpectedly. As another example:

- flags:
  - default: false
  - {name: [-fno-warn-incomplete-patterns, -fno-warn-overlapping-patterns]}

Here we have used default: false to say that any flags not explicitly allowed cannot be used. If someone accidentally checks in development code with {-# OPTIONS_GHC -w #-} then HLint will catch it. This restriction feature is particularly designed for code reviews.

What Might Have Broken

This release changes a lot of stuff. I am aware the following will no longer work:

  • The HLint2 API has been deleted - I don't think anyone was using it (the HLint and HLint3 ones remain unchanged). I'll continue to evolve the API in future releases.
  • The Haskell configuration file no longer has a way of importing other configuration files. At the same time I made it so the default configuration file and internal hints are always included, which I hopefully offsets most of the impact of ignoring hint imports.
  • I may have broken some other things by accident, but that's why there is a bug tracker.

At the moment the Haskell and YAML configuration files are both supported. However, I'll be phasing out the Haskell configuration in the future, and encourage people to move to the YAML. The conversion should be pretty simple.

Monday, April 03, 2017

Code Review Reviewed

Summary: I used to be mildly against code review on all merges. Now I'm for it. Code review is a good idea for knowledge sharing, not spotting bugs.

For my open-source projects, I accept pull requests from external contributors which I review, but my contributions are probably not routinely looked at by anyone else. I suspect most non-huge open-source projects follow the same pattern. For larger projects code review seems more common, but far from ubiquitous.

Until recently, I was in favour of occasional code review, e.g. towards the end of a project taking a look at the code. The problem with that approach is that it is hard to find the right time - at the end there is little appetite for large-scale refactoring and when the project is busy cranking out code there is no time and the code is still changing. While I was a fan of this idea in theory, it never worked in practice.

Some teams use code review on every merge to master, perhaps several times per person per day. That's something I used to disagree with, but I asked some smart people, and their explanations changed my opinion. The important realisation was thinking about what code review is for.

  • Checking the code works: NO. Code review is not about checking the code works and is bug free. I have tests, and leverage the type system, which is meant to convince me and other readers that my code is correct. For certain very sensitive bits a second set of eyes checking for bugs may be useful, but if all your code is that sensitive it will also be bug-ridden. However, code review may spot the absence or inadequacy of tests.
  • Checking simple rules and conventions: NO. Often projects have rules about which packages/extensions can be used, tab width and line length etc. While these checks can be carried out by a human, they are much better automated. Even when "code reviewing" students work at York University (aka marking) it quickly became clear that I was wasting time on trivialities, and thus wrote HLint to automate it.
  • High-level design: A BIT. Code review should think about the high-level design (e.g. should this be a web server or command line tool), but often the code is too detailed to properly elucidate these choices. High-level design should usually be done on a bug tracker or whiteboard before writing code.
  • Mid-level design: YES. Code review is often very good at challenging details around the mid-level design - e.g. does the choice of Text vs ByteString make sense, is there some abstraction that needs introducing. The author of some code is often heavily influenced by the journey they took to get to some point, by seeing code without that history a reviewer can often suggest a better approach.
  • Spreading knowledge: YES. Code review is great for spreading knowledge of the code to others in the team. Code review requires the code to be written in such a way that someone else can understand it, and ensures that there is someone else who is familiar with it. For larger projects that's invaluable when someone goes on holiday.
  • Team cohesion: YES Code review requires different members of the team to share their work with each other, and to have an appreciation of what other people are working through and the challenges it presents. It's all too easy to declare a problem "easy" without understanding the details, and code review removes that temptation.
  • Training: YES. Code review is also good for teaching new techniques and approaches to the submitter. As an example, some problems are trivial to solve with a generics library, yet some programmers aren't familiar with any - code review helps with ongoing training.

In contrast, I think the disadvantages of code review all revolve around the time required:

  1. It takes other peoples time to do the review, when they could be doing something else.
  2. It takes the submitters time waiting for a review - often the next step is hard to do without the previous step being agreed. As a result, I think code review work should be prioritised.
  3. As a consequence of the two previous issues, code review changes the "unit of work", leading to more changes in a single bundle.

These issues are real, but I think the benefit of knowledge sharing alone outweighs the cost.