NPRG075

Formal models of programming

Tomáš Petříček, 309 (3rd floor)
petricek@d3s.mff.cuni.cz
https://tomasp.net | @tomaspetricek

Lectures: Monday 12:20, S7
https://d3s.mff.cuni.cz/teaching/nprg075

History

Programming as mathematics

Programming in the late 1940s

ENIAC programmed by plugging wires and flipping switches

"The ENIAC was a son-of-a-bitch to program" - Jean (Jennings) Bartik

Mathematical science of computation

John McCarthy (1962)

In a mathematical science, it is possible to deduce from the basic assumptions, the important properties of the entities treated by the science.

What we want to answer

Does transformation preserve meaning?
Does translation procedure correctly translate?
Do two programs compute the same function?

Microalgol (1964)

Syntax and semantics of trivial Algol subset

\(micro(\pi,\xi)\) gives the final state of a program \(\pi\) run in a state \(\xi\)

"Description of the state of an Algol computation will clarify (..) compiler design"

Formal models

What are they good for?

Make sense of tricky language features
Prove properties of specific programs
Prove properties of the language
Make sure type system actually prevents bugs!

The definition of Standard ML (1990s)

Operational semantics
and type system for a complete language

Even language this simple had murky parts!


// Function: 'a -> 'a list
let callLogger =
  // List: 'a list
  let mutable log = []
  fun x ->
    log <- x :: log
    log

// Can we call this with:
callLogger 10
callLogger "hi"

Generalization and value restriction

ML makes top-level definitions polymorphic

Allowing that for values is unsound!

Soundness

Surely, we know better?

Are such problems in programming languages used today?
tinyurl.com/nprg075-unsound

Unexpected interactions!

Many Java extensions formalized
Formalizations with soundness proofs!
This is interaction between multiple features...

Semantics

Formal language definitions

Language semantics types

Axiomatic semantics
Define rules satisfied by individual commands
Denotational semantics
Assign mathematical entity to each program
Big-step operational semantics
Describe how terms reduce to values
Small-step operational semantics
Evaluation as gradual rewriting of terms

Language semantics types

Why small-step?

Easier to write than axiomatic or denotational

But harder to use for program equivalence

Good textbook and popular in PL research community

Works for programs that do not terminate

Semantics

Definition of an ML subset

Demo

Functions and numbers in F#

Expressions and evaluation

Evaluation rules

Functions and numbers

Functions and currying

Simplifying the rules

Conditionals and stuck state

Adding references

What did we learn?

Interesting aspects

Evaluation order of sub-expressions
Laziness of conditional expressions
What needs to be in the state

Interesting things left out

Data structures: records, unions, lists
Language features: recursion, exceptions
Hard things: Concurrency, input and output

ReactiveX

Programming with observables

Functional reactive programming

Classic functional style

Functional reactive animations (1990s)
Composing behaviours and events
Revised in the Elm programming style

Observables and events

Events that occur and produce values
Mouse moves, server notifications, user inputs, ...
Transformed using a range of operators

Functional reactive programming

Reactive animations (Elliott, 1997)

followMouseAndDelay u =
 follow `over` later 1 follow
  where
   follow = move (mouseMotion u) jake

How does it work

mouseMotion represents current mouse position
later delays time by X seconds
over overlays multiple animations

Reactive eXtensions

Events represented by Observable<T>

Produces values when something happen

Operators turn one or more observables into a new one

Demo

Programming with RxJS

Semantics

Formalizing observables

Minimal language with events

Demo

Lists and sequencing in F#

Modelling concurrency

Triggering events

Lists, sequencing and steps

Rules for event handlers

Events calculus

Focus on what matters

Lists, numbers and events only
No functions or recursion!
Probably still Turing-complete

What did we learn

Sequence of concurrent expressions
Selection of expression to be run
Scheduling when event is triggered

Alternative rules

Conclusions

Formal models

Useful design guide and for making formal claims

Explains core ideas of a system in a succinct way

The danger is producing languages that look
well on paper!

Language semantics types

Lambda calculus
Logic (1930s) but used for PL semantics (1960s+)
Pi calculus, CCS and CSP
Models of concurrent systems (1980s-90s)
Join calculus
Distributed asynchronous programming (1990s)
Programming language theory
Memory regions, effects and coeffects, locks, etc.