Tomas Petricek, The Alan Turing Institute
tomasp.net | tomas@tomasp.net | @tomaspetricek
What is this talk about?
Multi-level nature of programming concepts
Types
|
Monads
|
Locks
|
We always think, prove and implement!
Common sense types, formal monads, implementation locks
Programming concepts as scientific entities
Paper on gravity does not change how apples fall
Types across languages don't share the abstract
Types are used to provide auto-complete
We accumulate what we can implement
Variations on proofs and refutations
Proofs and refutations (Imre Lakatos)
Conceptual metaphors (George Lakoff & Rafael Núñez)
Originates at formal level
Pre-sheaves in category theory
Metaphors evolve from applications
Containers like lists and sequencing of effects
Implementations drift from theory
Artifacts such as do notation and LINQ
Background combines all levels
Type theory, common sense and implementation in Algol
Formalisms change to reflect use
Types as sets, types as relations, types as proofs
Implementations stretches the theory
Unsound type systems for documentation and auto-complete
Why understanding programming concepts matters
Multi-level nature
Conceptual, formal, implementation
Useful philosophy of science perspective
Where programs come from, scientific progress
Variations on proofs and refutations
Evolve across all three levels
Function or specification vs. physical implementation
Changes and evolves and stretched by implementations
Hard to cover all philosophy of science positions!
Scientific entities
There is some independent physical reality
Programming concepts
The physical is interlinked with the theoretical