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 -> ...