http://csunplugged.org/sorting-networks

communication

"Computer science is no more about computers than astronomy is about telescopes" - Dijkstra

Ideas, not technology

It's about tomorrow's jobs, not today's

Understanding the world, not just about jobs

Ideas, not technology Every child, not just geeks Educational not instrumental Discipline, not skill

2008 Computing at school 2010 CAS curriculum 2011 Shut down or restart report by Royal Society 2012 BCS invited to create a working group to draft the new Computing curriculu 2014 New curriculum launches

"You can say what you like, but it has to fit on two sides of A4"

Other subjects have centuries of experience; we have 5 years. Current practice is "gut feel". This is stupid. We should study what works and then do that.

Every teacher must come to an opinion about their students' understanding. They may do this informally, through project or programming work, or through asking them questions.

Where do they get these questions from? Often they just make them up.

Good questions are hard to write if you are an expert.

Project quantum

A corpus of high quality computing questions would be fantastically useful - to every teacher, year, and country.

A problem that has caused him a great amount of anxiety

Program |?| Proof

ASIL - automotive safety integrity level (lowest A, highest D)

Sensor input -> AI -> actuation

ASIL D requires that mathematical modelling or proof is done.

Program |extraction| Proof

Proof assistant Coq Agda Haskell

None of these are an option - Extraction target is C/C++

Could we extract the C program from a proof? There is some work on that. Generated code is terrifying, but "not to be inspected". Supposed to trust the extracting/generating code.

Programs, syntax (formalized, its structure and contents) vs semantics (modeled, what it means to run the program)

Denotational semantics - glue syntax to some meaning

u8 -> {x|x E N ^ x <= 255}

tableau - turnstile

A simple type theory isn't rich enough for reasoning about our programs

=> Dependent types

"realize a continuum of precision up to a complete specification of a programs behaviour" - Why Dependent Types Matter

http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf

CH correspondence

"Dependently typed programs are by their nature, proof carrying code"

Agda, or Idris

Lazily evaluated, non-deterministic memory management

=> Rust

defining nats inductively in Rust types

traits allow types to be treated like terms

example of the vector of size N in Rust

Rust doesn't have dependent types, we're wedging them in to through the type system. We don't trust the Rust compiler to enforce this.

Should use Coq, Agda, or Isabelle. So they wrote Agda <=> Rust.

Map the semantics of our Rust program into Agda, and use that to verify

Why do we care about this? Because we need UIs for ourselves. Data driven company. UIs that can dynamically transform and allow us to interact with the data.

Table, lots of data (~100k rows). Data is changing.

Jane Street use OCaml for everything! Including UIs.

A nice way of expressing UIs.

Not that different to that used in React or Elm.

... -> Action -> Model -> Virtual DOM -> ...

Lots of data in the initial render, but when things change they change in small ways. These small changes should be cheap to apply.

Model -> Virtual DOM -> DOM

Compute a diff between previous virtual DOM and the new one. Map that to changes to the DOM.

If the virtual DOM or model is big then it doesn't work so well.

Your computation as a dependency graph Based on Acar's Self Adjusting Computations

val map : 'a Incr.t -> ('a -> 'b) -> 'b Incr.t

Apply map once to build the incrementals for each sub part. Apply it again to convert it to the virtual DOM.

Map can fan out, but not fan in. Hence we use Map2, which takes two incrementals. Merge the two virtual DOMs.

val map2 : 'a Incr.t -> 'b Incr.t -> ('a -> 'b -> 'c) -> 'c Incr.t

Static graphs/structure.

A page that shows one or the other.

val bind : 'a Incr.t -> ('a -> 'b Incr.t) -> 'b Incr.t

Dynamic graphs. But somewhat limited.

• Map works for static structures
• Bind adds (limited) dynamism - whole new computations on the right, compromising incrementality.

How about incrementality sorting 10,000 things? It's not clear how you would do that.

How can we be dynamic and incremental?

val incr_map : ('k, 'v1, 'cmp) Map.t Incr.t -> ('v1 -> 'v2) -> ('k, 'v2, cmp) Map.t Incr.t

Overloading here:

Map the structure map the operation

let incr_map m f = let%map m = m in Map.map m f

where

let%map

is sugar from https://github.com/janestreet/ppx_let

Symmetric diff function on two maps, produces a sequence of Left, Right, or Unequal (both, but with different values)

Fast.

Take this idea and embed it in an incremental computation

Previous value

val diff_map : 'a Incr.t -> (('a * 'b) option -> 'a -> 'b) -> 'b Incr.t