Review: Verified Functional Programming in Agda

Agda is a dependently typed programming language. I’ve read about dependent types on and off for the past few years in magazine articles as well as discussed them a little with my collaborator Dan Ghica and others, but never really had the time to properly experiment until this Easter holiday. This book – by Aaron Stump – is interesting because it’s basic, practical, and jumps right into coding. I thought it would be good for someone like me who wants to play with the practice of dependent types and only delve into theoretical concerns as necessary or motivated to do so.

The book comes with its own Agda library, the Iowa Agda Library (IAL), a basic library of Booleans, lists, etc., simply written for the beginner to understand. It has a lot of exercises and code snippets based on that library which I found useful and relatively easy to follow.

The book assumes no functional programming expertise, and since I’ve done a (very) little bit of functional programming in Haskell in the distant past, this made the introductory material easy to follow and a useful revision aid.

Introductory Agda

The early parts of the book – Chapters 1 to 4 – are based on various data structures: Booleans, natural numbers, lists. Here the functional programming adds little to what I’ve seen before. The neat thing is the ability to use Agda as a theorem prover. This is what is described in the book as “external verification” – you write code and then you prove – separately – theorems about the code.

Firstly, let’s take a look at some example Agda code, taken from Chapter 4:


take : ∀{ℓ}{A : Set ℓ} → (n : ℕ) → 𝕃 A → 𝕃 A
take 0       _         = []
take (suc n) []        = []
take (suc n) (x :: xs) = x :: take n xs

There’s a few interesting things here already. Firstly, unicode! It feels surprisingly liberating to write unicode characters in code. Secondly the type declaration declares (via ∀), the function to be polymorphic – it operates on lists (𝕃 from IAL) of any type A (of any level ℓ within a hierarchy of type levels).

The real excitement comes when we start proving theorems. For example, given the function nthTail from IAL which returns all elements after the first n elements in a list (and the empty list if the list has fewer than n elements), we can write


ex46 : ∀{ℓ}{A : Set ℓ} (n : ℕ)(l : 𝕃 A) → (take n l) ++ (nthTail n l) ≡ l
ex46 0        _                           = refl
ex46 (suc n) []                           = refl
ex46 (suc n)  (x :: xs) rewrite ex46 n xs = refl

Here ex46 is just the name of my proof (it was Exercise 4.6 in the book). The type declaration for the function ex46 can be read as “I’ll produce a proof that concatenating (take n l) with (nthTail n l) just produces l for all natural numbers n and for all lists of elements of any type A. Here , taken from IAL, is propositional equality, and the only property of it we’re using is reflexivity; in fact the only inhabitant of this type is refl. The first two lines of the proof work because the definitions of take and nthTail are such that when the first argument is zero or the second argument is empty, the left and right hand side normalize to the same result, namely .l ≡ .l in the first case (.l being the name assigned to the second unnamed argument _) and [] ≡ [] in the second case. The third case explicitly uses induction: rewrite is a directive that applies the induction hypothesis ex46 n xs to the proof of ex46 (suc n) (x :: xs). Very pleasing!

Dependent Types Revealed

Chapter 5 is where we really start to see the power of dependent types. Up until this point, we’ve written functional programs and then proved properties about those programs. We have definitely used dependent types in the process, but they were somehow “invisible” to us as a user, and – at least for the exercises in the book – we could ignore the dependent-type based implementation without really affecting the usability of the approach. Chapter 5 shows how the proofs can be part of the programs themselves, using the type system to express the properties we wish to enforce. The simplest and clearest example given is a declaration of a vector datatype:


data 𝕍 {ℓ} (A : Set ℓ) : ℕ → Set ℓ where
[] : 𝕍 A 0
_::_ : {n : ℕ} (x : A) (xs : 𝕍 A n) → 𝕍 A (suc n)

Note here that a vector, unlike a list, has a specific length built into its type. As a result, you get various properties for free, for example Agda’s type system verifies that the length of the concatenation of two vectors is the sum of the individual lengths from a straight-forward definition of a concatenation operation; the code below type checks, and that’s all that necessary.


_++𝕍_ ∀{ℓ}{A : Set ℓ}{n m : ℕ} → 𝕍 A n → 𝕍 A m → 𝕍 A (n + m)
[] ++𝕍 ys = ys
(x :: xs) ++𝕍 ys = x :: (xs ++𝕍 ys)

A more complex example of Braun trees is described in detail in the book. These are binary trees where the data at a node has a value less than or equal to that of its children while the size of the node left and right subtrees are either equal or the left subtree is exactly one node larger than the right subtree. The author chooses to encode this latter property within the declaration of the Braun tree type, and then shows how to write code for tree insertion, deletion, etc.

I enjoyed this chapter, though it had me puzzling for quite some time over sigma types, a subtle and powerful idea that I think deserves a bit more discussion than the space given in the book; I ended up reading around this topic a bit before I felt comfortable. An example given considers a function that turns lists into vectors. Immediately we have a problem – what is the return type of this function? It should be (𝕍 A n) but n is not fixed! The solution presented is to return a type written in Agda as Σ ℕ (λ n → 𝕍 A n); an inhabitant of this type should be interpreted as “a pair consisting of a natural number and a function which, when applied to that natural number, returns the vector type we’re actually interested in.” This takes a little getting used to!

Type-Level Computation

Chapter 6, introduces the idea of proof by reflection, amongst other things. This looks super-powerful, and I’m motivated to dig further into this topic when I have the time. The author illustrates the concept by creating a list simplifier, which simplifies expressions on lists. By reflecting the operations on lists as corresponding constructors for list expressions, and then proving the soundness of the simplifier, he is able to use this soundness proof to, inter alia, prove properties about the operations operating on lists. The example is really interesting, though unlike in previous chapters of the book, it’s not really discussed in detail in Chapter 6, and you have to look carefully at the code accompanying the book to see how it all fits together.

The other primary example of Chapter 6 is a statically typed version of printf, the archetypal type-evasive function of my youth

int printf( const char *restrict format, ... );

Here, the author presents an example credited to Augustsson, showing that dependent types can come to the rescue essentially by providing a type for C’s “…” which depends on the format string.

The integer example from this chapter is the closest to my own interests, showing how integers can be defined using naturals in an interesting way: an integer is a natural together with a sign which is unit (trivial) if the natural is zero but has Boolean type otherwise, i.e. the type of the sign is dependent on the value of the natural, leading to the following type declaration and definition of ℤ [taken from here].


ℤ-pos-t : ℕ → Set
ℤ-pos-t 0 = ⊤
ℤ-pos-t (suc _) = 𝔹

data ℤ : Set where
mkℤ : (n : ℕ) → ℤ-pos-t n → ℤ

I had followed through the discussion in the book easily, but came totally unstuck when trying to implement a seemingly obvious exercise I set myself: prove that integer multiplication commutes using a pre-existing proof of the commutativity of multiplication over the naturals.

I had defined integer multiplication as:


_*ℤ_ : ℤ → ℤ → ℤ
_*ℤ_ (mkℤ 0 _)        _                = mkℤ 0 triv
_*ℤ_ (mkℤ (suc n) _)  (mkℤ 0 _)        = mkℤ 0 triv
_*ℤ_ (mkℤ (suc n) sn) (mkℤ (suc m) sm) = mkℤ ((suc n) * (suc m)) (sn xor sm)

where triv is the single inhabitant of the type.  I had therefore naively assumed that one could simply write the proof as:

*ℤcommutes (mkℤ 0 _)        (mkℤ 0 _) = refl
*ℤcommutes (mkℤ 0 _) (mkℤ (suc bN) _) = refl
*ℤcommutes (mkℤ (suc aN) _) (mkℤ 0 _) = refl
*ℤcommutes (mkℤ (suc a) sa) (mkℤ (suc b) sb) rewrite xor-comm sa sb | (*comm (suc a) (suc b)) = refl

However, this fails – for the final pattern – for a very interesting reason that was, however, totally incomprehensible to me at first. Agda reports:

𝔹 !=< ℤ-pos-t w of type Set
when checking that the type
(b a w : ℕ) →
w ≡ suc (a + b * suc a) →
(sa sb : 𝔹) →
mkℤ w (sb xor sa) ≡ mkℤ (suc (a + b * suc a)) (sb xor sa)
of the generated with function is well-formed

“Huh? ‘Generated with function?'”

Thus began a small odyssey of Easter holiday evenings spent learning how rewrites are implemented as withs, and how withs in turn are implemented using generated auxiliary functions. I found Norrell and Chapman’s tutorial, together with the good quality documentation provided me with the necessary additional background required to teach myself what was going on here and to produce a final, working proof:


*ℤcommutes : ∀ (a b : ℤ) → a *ℤ b ≡ b *ℤ a
*ℤcommutes (mkℤ 0 _)        (mkℤ 0 _)        = refl
*ℤcommutes (mkℤ 0 _)        (mkℤ (suc m) sm) = refl
*ℤcommutes (mkℤ (suc n) _)  (mkℤ 0 _)        = refl
*ℤcommutes (mkℤ (suc n) sn) (mkℤ (suc m) sm)
with m + n * suc m | *comm (suc n) (suc m)
... | .(n + m * suc n) | refl rewrite xor-comm sn sm = refl

I have mixed feelings about this experience. On the one hand, I’ve learnt a lot about Agda specifically (and dependent types in general) by being forced to go through this process to understand what’s going on under the hood. On the other hand, this seems like a lot of hoops to jump through for this simple proof, and the book under review didn’t have all the answers I was looking for to solve the exercise. I don’t see the latter point as a big deal, but if you’re going to do your explorations on holiday, make sure you have a wifi connection available so you can look beyond the book for help!

Selected Topics

The remainder of the book is eclectic but interesting.

Chapters 7 and 8 combine to produce a larger example piece of code – a Huffman coder / decoder. It’s good to see the ideas put into practice in a larger case study, of course, though these chapters were less interesting to me personally.

Chapter 9 really recaptured my attention, though! The author uses Agda’s types to reason about termination. He explicitly sets up a general datatype representing what it means for a relation DAG to not have any infinite chain of successor nodes starting from a given named node, something he calls a terminating relation. He then proves in Agda that > over ℕ is terminating in this sense. The chapter then goes on to apply this to producing a termination proof for a recursively defined division function. I’m aware of this kind of reasoning, and have even played a bit with tools making use of these ideas like Byron Cook et al.‘s Terminator. So it’s interesting to see this in the context of the type system of Agda where in fact it becomes rather important since all functions must terminate in Agda – otherwise none of the proofs discussed above make sense!

The final chapter of the book, Chapter 10, formalises some ideas in a particular logic within Agda, using Agda to prove soundness and completeness of the logic.

Conclusion

The book ends rather abruptly with Chapter 10 on intuitionistic logic and Kripke semantics. There is no rounding off, summarising lessons learnt or directions for future research or indeed practical programming advice.

Nevertheless, I learnt a lot from reading this book – and a lot more from doing its exercises! It’s given me an initial understanding of one of the most recently talked-about developments in programming. I’m left keen to try to apply this to some real-world problems in my research! Well recommended holiday reading.

Primary Assessment

Readers of this blog will know that I have been critical of the Government’s assessment system for the new National Curriculum in England [1,2,3]. I therefore greet the Secretary of State’s recently launched consultation over the future of primary assessment with a cautious welcome, especially since it seems to follow well from the NAHT’s report on the topic.

What is Statutory Assessment for?

The consultation document states the aim of statutory assessment as follows:

Statutory assessment at primary school is about measuring school performance, holding schools to account for the work they do with their pupils and identifying where pupils require more support, so that this can be provided. Primary assessment should not be about putting pressure on children.

Firstly, let me lay my cards on the table: I do think that school “performance” deserves to be measured. My experiences with various schools suggests strongly that there are under-performing schools, which are in need of additional support to develop their educational practice. There is a subtle but telling difference between these perspectives, my own emphasising support while the Government’s emphasising accountability. While some notions of accountability in schools appear uncontroversial, the term has recently  become associated with high-stakes educational disruption rather than with improving outcomes for our children. We can definitely agree that primary assessment should not be about putting pressure on children; unfortunately, I don’t believe that the consultation proposals seriously address this question.

Consultation Questions

In this section, I focus on the questions in the Government’s consultation on which I have a strong opinion; these are by no means the only important questions.

Q2. The EYFSP currently provides an assessment as to whether a child is ‘emerging, expecting [sic] or exceeding’ the level of development in each ELG. Is this categorisation the right approach? Is it the right approach for children with SEND?

Clearly the answer here primarily depends on the use of these data. If the aim is to answer questions like “how well-aligned – on average – are children with the age-related expectations of the early-years curriculum at this school?” then this assessment scheme is perfectly reasonable. Nor does it need to be tuned for children with SEND who may have unusual profiles, because it’s not about individual pupils, nor indeed for high attaining children who may be accessing later years of the national curriculum during their reception years. But if it’s about understanding an individual learning profile, for example in order to judge pupil progress made later in the school, then any emerging / expected / exceeding judgement seems far too coarse. It groups together children who are “nearly expected” with those well below, and children who are “just above expected” with those working in line with the national curriculum objectives for half way up the primary school – or beyond.

Q3. What steps could we take to reduce the workload and time burden on those involved in administering the EYFSP?

Teacher workload is clearly a key issue. But if we are talking seriously about how to control the additional workload placed on teachers by statutory assessment, then this is an indication that our education system is in the wrong place: there should always be next to no additional workload! Assessment should be about driving learning – if it’s not doing that, it shouldn’t be happening; if it is doing that, then it should be happening anyway! So the key question we should be answering is: why has the statutory framework drifted so far from the need to support pupils’ learning, and how can we fix this?

Q5. Any form of progress measure requires a starting point. Do you agree that it is best to move to a baseline assessment in reception to cover the time a child is in primary school (reception to key stage 2)? If you agree, then please tell us what you think the key characteristics of a baseline assessment in reception should be. If you do not agree, then please explain why.

[… but earlier …]

For the data to be considered robust as a baseline for a progress measure, the assessment needs to be a reliable indicator of pupils’ attainment and strongly correlate with their attainment in statutory key stage 2 assessments in English reading, writing and mathematics.

I agree wholeheartedly with the statement regarding the requirements for a solid baseline progress measure. And yet we are being offered up the possibility of baselines based on the start of EYFS. There is no existing data on whether any such assessment strongly correlates with KS2 results (and there are good reasons to doubt it). If the government intends to move the progress baseline from KS1 down the school, then a good starting point for analysis would be the end of EYFS – we should already have data on this, although from the previous (points-based) EYFS profile. So how good is the correlation of end-of-EYFS and KS2? Because any shift earlier is likely to be worse, so at least this would provide us with a bound on the quality of any such metric. Why have these data not been presented?

It would, in my view, be unacceptable to even propose to shift the baseline assessment point earlier without having collected the data for long enough to understand how on-entry assessment correlates with KS2 results, i.e. no change should be proposed for another 6 years or so, even if statutory baseline assessments are introduced now. Otherwise we run the risk of meaningless progress metrics, with confidence intervals so wide that no rigorous statistical interpretation is possible.

Q9. If a baseline assessment is introduced in reception, in the longer term, would you favour removing the statutory requirement for all-through primary schools to administer assessments at the end of key stage 1?

The language is telling here: “to administer assessments.” If this were phrased as “to administer tests,” then I would be very happy to say “yes!” But teachers should be assessing – not examining – pupils all the time, in one form or another, because assessment is a fundamental part of learning. So really the question is the form of these assessments, and how often they should be passed up beyond the school for national comparison. Here the issue is more about the framework of support in which a school finds itself. If a school is “left to its own devices” with no local authority or other support for years (a common predicament at the moment with the abolition of the Education Services Grant by the Government!) then it way well be too long to wait six-and-a-half years before finding out that a school is seriously under-performing. Yet if the school exists within a network of supportive professionals from other schools and local authorities who have the time and resource to dig deeply into the school’s internal assessment schemes during the intervening years, these disasters should never happen. A prerequisite for a good education system is to resource it appropriately!

Q11. Do you think that the department should remove the statutory obligation to carry out teacher assessment in English reading and mathematics at key stage 2, when only test data is used in performance measures?

I think this is the wrong way round. Schools should only be required to report teacher assessment (and it should be “best fit”, not “secure fit”); tests at Key Stage 2 should be abolished. This would be fully consistent with high quality professional-led, moderated assessment, and address the very real stress placed on both children and teachers by high-stakes testing schemes. Remember the consultation document itself states “Primary assessment should not be about putting pressure on children.”

Q14. How can we ensure that the multiplication tables check is implemented in a way that balances burdens on schools with benefit to pupils?

By not having one. This is yet another situation where a tiny sliver of a curriculum (in this case tedious rote learning of multiplication tables) is picked out and elevated above other equally important elements of the curriculum. Boaler has plenty to say on this topic.

Q15. Are there additional ways, in the context of the proposed statutory assessments, that the administration of statutory assessments in primary schools could be improved to reduce burdens?

The best way to reduce the burden on schools seems to be to more closely align formative and summative assessment processes. However, schools have been explicitly encouraged to “do their own thing” when it comes to formative assessment processes. The best way the Government could help here is by commissioning an expert panel to help learn from the best of these experiments, combining what has been learnt with the best international educational research on the topic, and re-introducing a harmonised form of national in-school assessment in the primary sector.

Best Fit or Secure Fit?

The consultation appears to repeat the Government’s support for the “secure fit” approach to assessment. The document states:

The interim teacher assessment frameworks were designed to assess whether pupils have a firm grounding in the national curriculum by requiring teachers to demonstrate that pupils can meet every ‘pupil can’ statement. This approach aims to achieve greater consistency in the judgements made by teachers and to avoid pupils moving on in their education with significant and limiting gaps in their knowledge and skills, a problem identified under the previous system of national curriculum levels.

The key word here is every. This approach has been one of the key differentiators from the previous national curriculum assessment approach. I have argued before against this approach, and I stand by that argument; moreover, there are good statistical arguments that the claim to greater consistency is questionable. We are currently in the profoundly odd situation where teacher assessments are made by this “secure fit” approach, while tests are more attuned with a “best fit” approach, referred to as “compensatory” in previous DfE missives on this topic.

However, the consultation then goes on to actually suggest a move back to “best fit” for writing assessments. By removing the requirement for teacher assessments except in English, and relying on testing in KS2 for maths and reading, I expect this to be a “victory for both sides” fudge – secure fit remains in theory, but is not used in any assessment used within the school “accountability framework”.

High Learning Potential

The consultation notes that plans for the assessment of children working below expectation in the national curriculum are considered separately, following the result of the Rochford Review. It is sad, though not unexpected, that once again no particular mention is given to the assessment of children working well above the expectation of the national curriculum. This group of high attaining children has become invisible to statutory assessment, which bodes ill for English education. In my view, any statutory assessment scheme must find ways to avoid capping attainment metrics. This discussion is completely absent from the consultation document.

Arithmetic or Mathematics?

Finally, it is remarkable that the consultation document – perhaps flippantly – describes the national curriculum as having been reformed “to give every child the best chance to master reading, writing and arithmetic,” reinforcing the over-emphasis of arithmetic over other important topics still hanging on in the mathematics primary curriculum. It is worth flagging that these changes of emphasis are distressing to those of us who genuinely love mathematics.

Conclusion

I am pleased that the Government appears to be back-tracking over some of the more harmful changes introduced to primary assessment in the last few years. However, certain key requirements remain outstanding:

  1. No cap on attainment
  2. Baselines for progress measures to be based on good predictors for KS2 attainment
  3. Replace high-stress testing on a particular day with teacher assessment
  4. Alignment of summative and formative assessment and a national framework for assessment
  5. Well-resourced local networks of support between schools for support and moderation

DATE 2017: Some Personal Highlights

This week I was away at the 2017 Design, Automation and Test in Europe Conference (DATE) in Lausanne, Switzerland, where my collaborator and former staff member Kevin Murray was presenting our joint work with Andrea Suardi and Vaughn Betz.

IMG_9542

In this blog post I note a couple of personal highlights from the conference.

Apart from Kevin’s paper, which I describe in accessible form in a previous blog post, Jie Han and Marc Riedel‘s tutorial on stochastic computation was thought provoking. It’s an old idea, which I’ve seen a few times, but it was interesting to catch up with the recent thinking in this area: results on synthesis using Bernstein polynomials and a de-randomisation of the logic.

The theme of approximate computing pervaded the conference. Newcastle had an interesting paper on approximate multiplication where multiple partial products are compressed by replacing (implicit) summation with Boolean or operations. This complements more traditional approaches like I’ve worked on, where we just throw away partial products. It seems like there could be a few interesting generalisations of this approach.

It was also, of course, great to see the many colleagues I often meet at these conferences, and to spend some time in the laboratory of Paolo Ienne and meeting his PhD student Lana Josipovic, who is doing some very interesting work on high-level synthesis.

EPFL also has possibly the best underpass in the world:

DATE remains one of the best conferences to catch up with the various diverse directions in which EDA researchers have gone in recent years.

Overclocking For Fun and Profit

This week at the Design, Automation and Test in Europe (DATE) conference, Kevin Murray is presenting some exciting work I’ve done in collaboration with Kevin, his supervisor Vaughn Betz at the University of Toronto, and Andrea Suardi at Imperial College.

I’ve been working for a while on the idea that one form of approximate computing derives from circuit overclocking. The idea is that if you overclock a circuit then this may induce some error. However the error may be small or rare, despite a very significant performance enhancement. We’ve shown, for example, that such tradeoffs make sense for image processing hardware and – excitingly – that the tradeoffs themselves can be improved by adopting “overclocking-friendly” number representations.

In the work I’ve done on this topic to date, the intuition that a given circuit is “overclocking friendly” for a certain set of input data has been a human one. In this latest paper we move to an automated approach.

Once we accept the possibility of overclocking, our circuit timing analysis has to totally change – we can’t any longer be content with bounding the worst-case delay of a circuit, because we’re aiming to violate this worst case by design. What we’re really after is a histogram of timing critical paths – allowing us to answer questions like “what’s the chance that we’ll see a critical path longer than this in any given clock period?” Different input values and different switching activities give rise to the sensitization of different paths, leading to different timing on each clock cycle.

This paper’s fundamental contribution is to show that the #SAT probem can be efficiently used to quantify these probabilities, giving rise to the first method for determining at synthesis time the affinity of a given circuit to approximation-by-overclocking.

Playing with L-Systems

For today’s session of the math circle I jointly run for 5-7 year-olds, we got the kids to play with Lindenmayer Systems (L-Systems for short). L-Systems can be used as compact representations of complex geometric shapes, including fractals. The aim of the session was for children to understand that simple formulae can describe complex geometric objects, building on the intuition that properties of shapes can be described algebraically that we got through a previous session on symmetry and algebra.

I stumbled across this excellent L-System generator on the web, which was perfect for our needs as we didn’t need to install any software on the school laptops. After illustrating how the Koch Snowflake could be generated, we simply let them loose to experiment, suggesting that each time they set the number of iterations to 1 before exploring a greater depth of iteration. They seemed to really enjoy it. On a one-to-one basis, we discussed the reason that various formulae generated their corresponding shapes, trying to embed the link between the equations and the graphical representation, but the main emphasis was generating visually pleasing images.

Here are some of the curves they produced. In each case, the caption is of the form: number of iterations, angle, axiom, production rule.

I would have liked to have the time to discuss in more depth why the curve that appeared to fill the triangle had no white space visible.

Once we had finished, we finally drew together where I presented a simple L-System for the Sierpinski Triangle, an object they’d seen before in a previous session. There were several exclamations of awe, which are always great to hear!

Concurrent Programming in High-Level Synthesis

This week, my student Nadesh Ramanathan presents our FPGA 2017 paper “Hardware Synthesis of Weakly Consistent C Concurrency”, a piece of work jointly done with John Wickerson and Shane Fleming.

High-Level Synthesis, the automatic mapping of programs – typically C programs – into hardware, has had a lot of recent success. The basic idea is straightforward to understand, but difficult to do: automatically convert a vanilla C program into hardware, extracting parallelism, making memory decisions, etc., as you go. As these tools gain industry adoption, people will begin using them not only for code originally specified as sequential C, but for code specified as concurrent C.

There are a few tricky issues to deal with when mapping concurrent C programs into hardware. One approach, which seems modular and therefore scalable, has been adopted by LegUp: schedule threads independently and then build a multithreaded piece of hardware out of multiple hardware threads. This all works fine, indeed there is an existing pthreads library for LegUp. The challenge comes when there’s complex interactions between these threads. What if they talk to each other? Do we need to use locks to ensure synchronisation?

In the software world, this problem has been well studied. The approach proposed by Lamport was to provide the programmer with a view of memory known as “sequentially consistent” (SC). This is basically the intuitive way you would expect programs to execute. Consider the two threads below, one on the left and one on the right, each synthesised by an HLS tool. The shared variables x and y are both initialised to zero. The assertion is not an unreasonable expectation from a programmer: if r0 = 0, it follows that Line 2.3 has been executed (as otherwise r0 = -1). We can therefore conclude that Line 1.2 executed before Line 2.2. It’s reasonable for the programmer to assume, therefore that Line 1.1 also executed before Line 2.3, but then x = 1 when it is read on Line 2.3, not zero! Within a single thread, dependence analysis implemented as standard in high-level synthesis would be enough to ensure consistency with the sequential order of the original code, by enforcing appropriate dependences. But not so in the multi-threaded case! Indeed, putting this code into an HLS tool does indeed result in cases where the assertion fails.

 

mp-fix1

My PhD student’s paper shows that we can fix this issue neatly and simply within the modular framework of scheduling threads independently, by judicious additional dependences before scheduling. He also shows that you can improve the performance considerably by supporting the modern (C11) standard for atomic memory operations, which come in a variety of flavours from full sequential consistency to the relaxed approach natively supported by LegUp pthreads already. In particular, he shows for the first time that on an example piece of code chaining circular buffers together that you can get essentially near-zero performance overhead by using the so-called acquire / release atomics defined in the C11 standard as part of a HLS flow, opening the door to efficient synthesis of lock-free concurrent algorithms on FPGAs.

As FPGAs come of age in computing, it’s important to be able to synthesise a broad range range of software, including those making use of standard concurrent programming idioms. We hope this paper is a step in that direction.

National Funding Formula

This post contains my personal response to the DfE’s second round consultation on the national funding formula for schools. Individuals, organisations, schools, etc., should feel free to reuse my response. My response is based on my earlier – and lengthier – analysis of the DfE’s proposals, which goes into much more depth. Those interested beyond the specific questions being asked by the DfE should consult the earlier post too.

Please note that consultation responses need to be submitted by 22nd March 2017 and can be done online. Please submit a response, even a partial one. This issue is too important to be ignored!

Q1. In designing our national funding formula, we have taken careful steps to balance the principles of fairness and stability. Do you think we have struck the right balance?

No.

The introduction of a funding floor is a fundamentally unfair approach. The stated purpose of the national funding formula was to provide fairness and end the “postcode lottery”. A funding floor, as envisaged by the consultation document, entrenches the postcode lottery in the current funding environment rather than eliminating it.

Q2. Do you support our proposal to set the primary to secondary ratio in line with the current national average?

Yes.

In the absence of further evidence, this seems like a sensible approach. However I am disappointed that further evidence has not been sought, e.g. a study of the relative primary/secondary performance across different local authorities with different ratios in place. By introducing the NFF, such studies will no longer be possible and so the Government is missing an opportunity to base these decisions on hard evidence.

Q3. Do you support our proposal to maximise pupil-led funding?

No – you should increase school-led funding compared to the current national average

This approach fundamentally ignores the different shape and makeup of schools. It would only be a reasonable approach if costs were all equally pupil-led. Instead, I support the principle of equalising disposable income per pupil. Once fixed costs are taken into account, this principle is opposed to that of maximising pupil-led funding.

Q4. Within the total pupil-led funding, do you support our proposal to increase the proportion allocated to the additional needs factors?

No – allocate a lower proportion to additional needs.

I would have said “don’t know” if given an option here, because the DfE has not presented any evidence that increasing this proportion is an appropriate decision. Equally, I do not have evidence that reducing it would be a good decision. Given local authorities central role in understanding local educational additional needs, in the absence of additional evidence, I believe LA averages should be used, which corresponds to a lower proportion compared to the proposals.

Q5. Do you agree with the proposed weightings for each of the additional needs factors?

Q5a. Deprivation – Pupil Based

No – allocate a higher proportion.

A number of studies, e.g. [1], have shown a stronger link between pupil-based deprivation indices and educational disadvantage than between area-based deprivation indices and educational disadvantage. Once again, a boundary discontinuity study would have been helpful, and I am disappointed that this work has not been undertaken.

[1] C. Crawford and E. Greaves, “A comparison of commonly used socio-economic indicators: their relationship to educational disadvantage and relevance to Teach First,” IFS Report R79, 2013.

Q5b. Deprivation – Area Based

No – allocate a lower proportion

See answer to “Deprivation – Pupil based”

Q5c. Low Prior Attainment

No – Allocate a lower proportion

There is simply no justification given in the consultation document for nearly doubling the funding going through this factor. It is frankly shocking that such radical changes can be proposed with no evidence presented in their favour.

No matter what proportion is decided upon for the initial implementation of the NFF, the Government should commit that in the future, should prior attainment metrics rise nationally, any funding lost to schools through the low prior attainment factor should be recycled into the APWU factor.

Q5d. English as an Additional Language

No – allocate a lower proportion

LAs have chosen to allocate an average of 0.9%. The proposal is to increase this to 1.2%. No evidence is presented to support this change, therefore I cannot support it.

On a related matter, for a fixed pot of EAL funding, there is an argument to be had over whether children would benefit more from considerable funding in year 1 for intensive English tuition to allow them to access the curriculum, rather than more “smeared out” three year funding at a lower level per year. Once again, it would be useful to see the research that suggests that one or the other approach actually reaps the greatest benefit before mandating EAL3.

Q6. Do you have any suggestions about potential indicators and data sources we could use to allocate mobility funding in 2019-20 and beyond?

None

Q7. Do you agree with the proposed lump sum amount of £110,000 for all schools?

7a. Primary

No – Allocate a higher amount

In order to ensure the principle of equal disposable income per pupil, the purpose of the lump sum should not be to “contribute to the costs that do not vary with pupil numbers” but rather to “be a genuine reflection of the costs that do not vary with pupil numbers”

7b. Secondary

No – Allocate a higher amount

See answer to “Primary”

Q8. Do you agree with the proposed amounts for sparsity funding of up to £25,000 for primary and up to £65,000 for secondary, middle and all-through schools?

Q8a. Primary

No – Allocate a lower amount

With a properly funded lump sum that reflects the costs that do not vary with pupil numbers, there is no need for a sparsity factor. Need for a sparsity factor is an admission that there are pupils in “non sparse” areas who are being deprived of appropriate disposable funding.

Q8b. Secondary

No – Allocate a lower amount

See answer to Primary

Q9. Do you agree that lagged pupil growth data would provide an effective basis for the growth factor in the longer term?

No comment

Q10. Do you agree with the principle of a funding floor?

No

The introduction of a funding floor completely eliminates the stated purpose of the NFF. It reintroduces and – worse – codifies – a postcode lottery based on historical funding rates.

Q11. Do you support our proposal to set the funding floor at minus 3%?

No

I do not support the funding floor.

Q12. Do you agree that for new or growing schools (i.e. schools that are still filling up and do not have pupils in all year groups yet) the funding floor should be applied to the per-pupil funding they would have received if they were at full capacity?

No

I do not support the funding floor

Q13. Do you support our proposal to continue the minimum funding guarantee at minus 1.5%?

No – the minimum funding guarantee should be higher (i.e. restrict losses to less than 1.5% per pupil in any year)

I strongly support the existence of a MFG as a way of phasing in funding changes. However, in the present financial climate a MFG of -1.5% is problematic coming on top of other issues such as the radical reduction in the education services grant to local authorities and the apprenticeship levy.

Q14. Are there further considerations we should be taking into account about the proposed schools national funding formula?

As a general principle, deviations from a move to average values across LA funding formulae should be justified and evidence-based. I have provided a lot more questions for consideration in a blog post at https://constantinides.net/2016/12/16/national-funding-formula-for-schools-a-critique/

Q15. Do you agree that we should allocate 10% of funding through a deprivation factor in the central school services block?

No Answer

I am disappointed the options in this questionnaire do not allow me to state “not sure”, because – once again – no evidence has been provided to justify the figure of 10%. What I can say confidently is that the overall level of central school services block is far too low. In effect schools are seeing a significant cut to their funding because they will need to fund services previously provided through the Education Services Grant.

Q16. Do you support our proposal to limit reductions on local authorities’ central school services block funding to 2.5% per pupil in 2018-19 and in 2019-20?

No – limit reductions to less that 2.5% per pupil per year

In line with my school-level comments on MFG, it is important to have transitional arrangements in place. Given the radical cut to the Education Services Grant, it is not clear why the proposed limit of 2.5% is so much greater than the school MFG rate of -1.5%.

Q17. Are there further considerations we should be taking into account about the proposed central school services block formula?

No Answer

Algebra and symmetry for 5-7 year-olds

At the encouragement of one of the teachers, I have resumed the math circle I was running a few years ago, jointly with her. Previous posts can be found here. This time we are targeting some of the youngest primary school children. So far, I’ve attended two sessions. In the first, we played with Polydron and I mainly used the session to observe the children and see what they’re capable of. In the second – described here – we experimented with symmetry.

Before the session, we created a few cardboard templates of three well-defined shapes, numbered 1, 2, and 3 in the picture below.

IMG_9197 (1).jpg

We told the children that we would be exploring a way of describing shapes as codes, and first had them cut out several copies of the shapes from coloured paper. This was not as easy as I had hoped – the children varied considerably in speed and accuracy of cutting.

We then told them that there were two operations that could be written down in our code, “next to”, written “;” meaning “the thing on the left of the semicolon is placed immediately to the left of the thing on the right” and “F” meaning “flip the shape in a vertical axis”. They seemed to understand this quite easily, and had no problems coming up and seeking clarification of any points. I hadn’t considered that they had not encountered the semicolon before, though, but this was not a problem, even if it was rendered more like a “j” in most of their written formulae.

We asked them to construct a couple of shapes, such as 2;F2 and F1;2, and then experiment with their own. They seemed to have a lot of fun, and the lower part of the photograph shows some that they were keen to show us when we reconvened in a circle on the carpet.

The children noticed that some shapes such as 2;F2 and F2;2 were symmetric, whereas some were not. I pointed out that nobody had tried to construct a shape such as FF1, and asked what that might look like. Several children correctly identified that FF1 would be indistinguishable from 1, so I wrote “FF1 = 1”, and I think I saw a flicker of an “ah ha!” moment in at least one child who seemed excited by the use of equations here.

At this point we ran out of time in our 1hr session. I would like to take this simple algebra further. In particular, I would like to get them to explore:

  • the generalisation from the observed FF1 = 1 to ∀x.FFx=x.
  • the observation that symmetry in a vertical mirror line corresponds to the statement Fx = x
  • the observation that all shapes of the form x;Fx are symmetric, and relate this to the algebraic definition of symmetry
  • the property F(x;y) = Fy;Fx

For those of a mathematical bent, these are the properties of a semigroup with involution.

I enjoyed myself, and I think the children did too!

POPL and VMCAI 2017: Some Highlights

Last week I was in Paris attending POPL 2017 and co-located events such as VMCAI. This was my first time at POPL, prompted by acceptance of work with John Wickerson. Here are some highlights and observations from my own, biased, position as an outsider to the programming languages community.

Polyhedral analysis

Due to my prior work with linear programming and polyhedral analysis, the polyhedral talks were particularly interesting to me.

Maréchal presented an approach to condense polyhedral representations through ray tracing, which seems to be of general interest.

While in general, polyhedral methods represent some set as \{x | Ax \leq b\} where A and b are parameters, there are various restricted approaches which more efficiently fix A and only allow $b$ as parameters. Seladji presented a technique to try to discover such good “templates” via Principal Component Analysis. I suspect that this is equivalent to an ellipsoidal approximation of the polyhedron in some sense.

Singh, Püschel, and Vechev presented an interesting method to speed up polyhedral abstract domain computations by partitioning, resulting in a much faster tool.

SMT Solvers

An interesting paper from Jovanović presented a nonlinear integer arithmetic solver which looks genuinely very useful for a broad class of applications.

 

Heroics with Theorem Provers

Lots of work was presented making use of Coq, some of which seemed fairly heroic to me. Of particular interest, given my work on non-negative polynomials for bounding roundoff error, was a Coq tactic from Martin-Dorel and Roux that allows the use of (necessarily approximate) floating-point computation in ways I’ve not seen before, essentially writing a sum-of-squares polynomial p \approx z^T Q z as p = z^T Q z + z^T E z and showing that Q+E is positive semidefinite for some small E.

Weak Memory

John presented our work on automatically comparing memory models, which seemed to be well received.

img_9144

 

Numerics

Chiang et al. presented a paper on rigorous floating-point precision tuning. The idea is simple, but elegant: perform error analysis with individual precisions as symbolic variables and then use a global optimization solver to look for a high-performance implementation. Back in 2001, I did a very similar thing but for a very limited class of algorithm (LTI systems) in fixed-point rather than floating-point and using noise power rather than worst-case instantaneous error as the metric of accuracy. However, the general setting (individual precisions, an explicit optimization) are there, and it is great to see this kind of work now appearing in a very different context.

 

Cost Analysis

There were a couple of papers [Madhavan et al., Hoffmann et al.] I found particularly interesting on automated cost analysis.

 

Community differences

As an outsider, I had the opportunity to ponder some interesting cultural differences from which the various research communities I’m involved with could potentially learn.

Mentoring: One of the co-located workshops was PLMW, the Programming Languages Mentoring Workshop. This had talks ranging from “Time management, family, and quality of life” to “Machine learning and programming languages”. Introductory material is mixed with explicitly nontechnical content valuable to early career researchers. Co-locating with the major conference of the field, I would imagine makes it relatively easy to pull in very high quality speakers.

Reproducibility: POPL, amongst other CS conferences, encourages the submission of artifacts. I am a fan of this process. While it doesn’t quite hit the holy grail of research reproducibility, it takes a definite step in this direction.

National Funding Formula for Schools: A Critique

England’s Department for Education released its long-awaited Phase 2 of the consultation on a national funding formula on the 14th December 2016. I have been heavily involved in determining the funding formula for schools in one of the most diverse English local authorities, and so have some detailed thoughts on this process. As a prelude to my own response to the funding formula consultation, I thought it might be helpful to others to lay out my comments against the paragraphs of the Government’s consultation document as a “guide to reading”. I have focused on the areas I know best, which relate to funding arriving at schools rather than proposed funding to be distributed to LAs still, such as funding for growth, central school services, etc.

The DfE seems to be considering two quite distinct drivers for the decisions being proposed. Many decisions use LA formulae and averages between LAs to drive appropriate funding formulae. Elsewhere, clear politically-driven approaches come through – the drive to increase the proportion of funding going into pupil-led factors, etc. These have been presented in a jumbled up fashion that makes it hard to understand the relative impact of these considerations. It would be a relatively straight-forward mathematical task to set up and solve an optimization problem to minimize school funding turbulence when moving to a funding formula using these formula elements. It is disappointing that the DfE has not done this to at least provide an element of transparency in the proposals, as deviation from any such minimal-turbulence formula should indicate the presence of evidence being used to drive a decision. Put plainly: changes to school funding should be either to even up funding between LAs or to achieve a certain outcome.

I have chosen to blog here about the nuts and bolts, and save a formal consultation response, or any overall conclusions, for a future post. I hope my fellow consultation readers and I can have a conversation about these points in the mean time.

As a result of this decision, the remainder of this post is fairly lengthy, and will only make sense if you read it alongside the DfE’s paper. Happy reading!

The Gory Details

1.12 and again in 2.20. This is flawed reasoning. The DfE is correct that if pupils tend to share deprivation (or any other) characteristics, then allocation of funding through these factors achieves the same end result as allocation through basic per-pupil funding. But this is true either in areas of high uniform deprivation or in areas of low uniform deprivation. As a result, the appropriate methodology to use LA formulae to determine the desirable size of deprivation factor would be to specifically look at the formulae of LAs with wide variations in deprivation from school to school, providing a low weighting to formulae of LAs with less varying deprivation, not to simply assume that deprivation funding needs to increase. (Which, incidentally, I am not against, I just want to see evidence before making decisions. Typically such evidence comes from boundary discontinuity studies between schools near borders of LAs. We therefore have a once-in-a-generation opportunity to grasp the nettle and do this properly, before a national funding formula arrives and discontinuities – and hence evidence – disappears.)

1.16. The lump sum is a critically important factor in school funding, especially in areas with schools of widely varying size. The DfE claim that they “cannot see any clear patterns in the specific lump sum values.” Yet it is unclear what analysis has been conducted to discern a pattern. I would not expect any pattern to emerge from the analysis published, because no correlation is looked for between lump sum and school size variability. Nor can this be extracted from the published LA pro-forma summaries. The DfE does note a pattern in this paragraph that a majority of LAs set the same lump sum for secondaries as for primaries, but this could well be only because it was a requirement for the first year of the recent reforms to funding formulae!

2.7 – 2.9 and 2.51-2.56. It is very clear that the DfE has set the maximisation of funding allocated through pupil-led factors as an objective, as evidenced by the title of this section and the explicit references to the aim within the paragraphs. The claim in Paragraph 2.8 is that this is to ensure that “funding is matched transparently to need”. I do not believe this maximisation of funding through pupil-led factors is consistent with matching funding to need. If the Government truly wishes to be fair in its distribution of funding, then with similar school population characteristics, every school should receive the same disposable per pupil funding. Unless lump sums are set to reflect the genuine fixed costs of running a school then in practice the Government will be creating significant inequality of access to education by ensuring that pupils attending large schools attract a significantly greater disposable per pupil funding.

2.13. While I recognise the potential need for an increase in funding when moving from KS1/2 to KS3 and KS4, reception classes are also generally more expensive to run than KS1/2 classes due to the nature of the curriculum in R. By setting a single rate across the primary sector, the funding formula will differentially impact negatively on infant schools, where reception classes make up a greater proportion of the children.

2.16. The consultation document claims that “reception uplift” has “a very small impact on schools’ budgets.” I would like to see what evidence has been used to come to this conclusion. No doubt it has a very small impact on overall school budgets nationally, but I expect that for small schools it could have a considerable impact. Maintained schools have to wait for about 7 months before their census data results in funding changes; academies for nearly a year. In a school with 100 pupils, having 5 more pupils than expected should rightly result in a significant “reception uplift.”

2.21. No justification is given for the figure of 18% given for additional needs factors. The text implies that this goes beyond LA averages and is a result of a conscious Government decision to increase AEN funding – such a decision should be evidence based.

2.26. Some “magic numbers” appear here also: 5.4% for pupil-level deprivation (FSM/FSM6) versus 3.9% for area level (IDACI). These numbers appear to have been plucked out of the air. Presumably there is some statistical evidence to support these figures – it would have been useful to have this sent out with the consultation.

2.28. This is confused. The claim seems to be that Ever6 FSM rate should be higher at secondary schools than primary schools because (i) the overall primary:secondary ratio is less than 1 (so what?) and (ii) the Pupil Premium is the other way round. But the DfE also sets the pupil premium rate (and why are these two not combined anyway since they’re both Ever6 based?) It seems that those setting the Pupil Premium rate want to tug the ratio one way and those setting the funding formula want to pull it back the other way. Most odd.

2.33. The IDACI index is being used in a questionable way here. An IDACI index is a probability that a given child, chosen at random from a geographic area, lives in an income-deprived household. It is not a measure of the severity of deprivation. Thus I can see no justification for funding being allocated by IDACI score in anything other than a purely proportional way, e.g. a child living in an area with IDACI score 0.8 should surely attract twice the IDACI funding of a child living in an area with IDACI score 0.4. Yet looking at Figure 5, we can see that children in Band C (IDACI 0.35 to 0.4) attract the same funding as those in Band D (IDACI 0.3 to 0.35). This makes no sense to me. As an aside, the banding also makes very little sense – why classify pupils into bands if you already know the IDACI score of that pupil’s address: just use it directly, avoiding cliff edges of over/under-funding around the band’s boundaries.

2.34. In line with my comments on 2.21 and 2.26, the “magic number” here is even more alarming. The DfE have looked at how much LAs allocate to low prior attainment (4.3%) and decided to nearly double this to 7.5%. The only justification given for this radical shift is that KS2 attainment is a good predictor for attainment at secondary school. There are several holes in this argument. Firstly, what is “prior attainment”? For primary schools, this used to be EYFS points scores. Then it became whether a child achieved a Good Level of Development in EYFS. Now it is likely to be based on a totally different on-entry baseline assessment in Reception. None of these are comparable, and the baseline Reception assessments are very much questionable and under review at the moment. Secondly, for secondary schools prior attainment means KS2 results. The same KS2 results that have changed so radically in 2016 that we have no knowledge whether these are likely to be good predictors for secondary school performance. Thirdly, even if we ignore these serious methodological concerns, correlation between poor attainment (actually it should be SEN) and prior attainment is cause for a factor greater than zero. Simply no justification is given for why this factor should be doubled. Perhaps it should, perhaps it shouldn’t. Why?

2.42. The move to use EAL3, i.e. funding is attracted for children with English as an Additional Language for the first three years of their education is an interesting one. Currently LA practice varies here. For a fixed pot of EAL funding, there is an argument to be had over whether children would benefit more from considerable funding in year 1 for intensive English tuition to allow them to access the curriculum, rather than more “smeared out” three year funding at a lower level per year. Once again, it would be useful to see the research that suggests that one or the other approach actually reaps the greatest benefit before mandating EAL3.

2.43. More magic numbers here: uplift from 0.9% to 1.2%. Why? Evidence?

2.52. This paragraph makes it clear that the proposal is explicitly to starve small schools of funding, by purposely under-funding the lump sum, in order to ensure that they “grow, form partnerships and find efficiencies.” Rather than starving schools of funds, it might be better properly fund the lump sum while providing time-limited financial enticements for schools to merge where that is possible, as is currently the case.

2.53. There is a methodological error in this paragraph. They state that they looked for a correlation between average school size and lump sum size and found none. Nor should they expect to find one. Imagine LA1 with schools each of 100 pupils and LA2 with schools each of 1000 pupils. There will be no difference in allocation of funding between schools in these LAs no matter what lump sum value is used. However if we now imaging LA3 where half the schools have 100 pupils and half have 1000 pupils, then the impact of lump sum changes will be dramatic here. So the correlation should be with the variation in school size, not with the average school size.

2.57. A sparsity factor is only a sensible option given the choice to under-fund fixed costs in a lump sum. If these were properly funded, a sparsity factor would be unnecessary.

2.59. The detailed calculations for the function of the sparsity factor are omitted from the consultation document – instead a link is provided to another document. The functioning leaves a lot to be desired. For example, primary schools are eligible if they have an average of less than 21.4 children per year group and the average distance between this school and their next-nearest school is at least two miles. The first of these criteria is essentially an admission that schools will less than one form entry are underfunded under the national funding formula. The second is more complex but equally serious, especially for small village schools sitting on the edges of towns. Imagine two schools, separated by a little more than two miles. It may well be that between the two schools is an area of dense population while following the line connecting these two schools out into the countryside leads to very sparsely populated areas. The distance for the children at the countryside end might be much more than 2 miles, yet the average will be less than two, and the school will not attract funding. If thresholds of distance must be used, why is it done on average distance rather than the number of pupils for whom that distance is more than the threshold? Finally, these thresholds necessarily lead to unfairness across the two sides of the threshold. If the lump sum were set to a value reflecting the fixed costs of running a school, none of this tinkering would be necessary.

2.60. The steep tapering proposed for the primary sparsity factor is grossly unfair to schools with average year group sizes around 25 – they get none of the benefit compared to their colleagues with smaller classes, yet they see the full impact of an under-funded lump sum which can be safely ignored by large primaries.

2.61. Even if we accepted the sparsity factor, the maximum value of £25k for primaries on top of the £110k lump sum still under-represents the fixed costs of running a school. Meanwhile, the use of a greater lump sum of £65k for secondaries seems inconsistent with the simplification proposed to use a single lump sum across all phases.

2.77 – 2.79. This part of the consultation, on area cost adjustment, refers to a technical note that does not yet appear to have been published on the consultation website. I reserve judgement on this issue, noting that the devil is likely to be in the detail, and that any methodology for taken into account labour market costs needs to avoid cliff edges where schools on one side of an artificial geographical boundary benefit significantly compared to those on the other, an issue the national funding formula was supposed to address.

2.81-2.82. It is of course welcome that any reduction in school budgets is phased in over time so that schools are able to cope with “the pace […] of those reductions.” However, it is not very clear what this means in practice. What does it mean for a school to “cope” with its reduction in funding – does it mean a reduction in expenditure with negligible loss in educational outcomes, or with “acceptable” loss in educational outcomes? If the latter, what is acceptable? If the former, what evidence do we have that the current MFG of -1.5% per annum has negligible impact on educational outcomes?

2.83-2.85. It is far less clear that any kind of “floor” is an equitable way of smoothing change, indeed it goes against the very aim of an equal funding formula for all. Some schools will receive more funding simply because they historically did, and others will therefore receive less as a result, from any fixed education funding pot. If a floor is required in order not to damage school performance in the long run, this suggests that funding reductions implied by the national funding formula are simply unsustainable in those schools. Therefore instead of clamping maximum loss to 3%, the DfE should be asking why some schools lose more than 3% and whether this is justifiable for those schools. If not, the formula is at fault and should be changed for all schools, not just those below -3%.

2.86. By maintaining the floor as a per pupil funding guarantee, the Government could potentially introduce severe differentials between schools. In particular in areas of high existing lump sum where there are some small schools that grow to be of comparable size to large schools, the formerly small school would be very significantly over-funded compared to its neighbour, for no good reason.

3.11. The consultation states here that “we have considered carefully the potential impact on pupil attainment in schools likely to face reductions as a result of these reforms,” yet this analysis is not presented. Instead we are simply told that “we see excellent schools at all points of the funding spectrum,” which is no doubt true but fairly meaningless when it comes to assessing the educational impact. A good starting point would be to look at what correlation exists between disposable income per pupil, i.e. per pupil funding once realistic fixed costs are subtracted, and progress measures at the school.