msgodf/sl2018.md

Strange Loop 2018 notes

SPJ keynote

http://csunplugged.org/sorting-networks

communication

Myth 1. it's all about computers

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

Ideas, not technology

Myth 3. it's all about jobs

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

Understanding the world, not just about jobs

Summary

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

The UK journey

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"

Lesson 2. Get high-stakes examination rights

Lesson 3. Loving our teachers

Lesson 4. spend a tiny fraction of research

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.

Lesson 5. Leverage formative assessment

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.

Proof theory impressionism: Blurring the Curry-Howard line - Dan Pittman

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

Program |extraction| Proof

Proof assistant Coq Agda Haskell

Not an option - Extraction target is C/C++

Could we extract the C program from a proof? There is some work on that.

None of these