This was the final lecture for the course, directed in particular at visiting students who will be taking an exam shortly: with some general information on assessment practices, advice on exam technique, and specific details on the exam structure for this course. I also went through some example questions from previous exams, circulated earlier.
Continue reading Lecture 20: Exam Review
Category Archives: Lecture Log
Guest Lecture: Maria Gorinova
Probabilistic Programming:
What is it and how to improve it?
Maria Gorinova
3–4pm Tuesday 29 November
Drummond Library
G.10 Geosciences
Lecture 18: Concurrency and More in Rust
This afternoon’s lecture completed the review of Rust with an exploration of how references and ownership interact with threaded concurrency.
Continue reading Lecture 18: Concurrency and More in Rust
Lecture 17: Traits and References in Rust
Today’s lecture presented the core of Rust’s claim to provide safe systems programming: the use of move semantics, reference ownership and borrowing to provide precise and powerful memory-safe programming without runtime overhead. The features that provide this form a detailed deconstruction of what in other languages would be objects, but in Rust are carefully prised apart, each treated separately for their individual contribution. I also included a number of pictures of food to illustrate this.
Guest Lecture: Andrew Kennedy
The Hack Programming Language:
Types for PHP
Andrew Kennedy
3–4pm Friday 18 November
Gaddum Lecture Theatre G.8
1 George Square
Facebook’s main website, ads platform, and much of its internal tooling is implemented in PHP, a language not known for elegance or best practice in programming language design. (See http://phpsadness.com, for example.) Over the last three years Facebook has embarked on an ambitious project to migrate its code base to Hack, which takes the syntax of PHP, removes the worst features, and adds static typing and modern constructs for asynchronous programming and typed UI components. In this talk I will focus on Hack’s type system, which combines ML-like type inference, object-oriented generics in the style of C# or Java, and flow-based typing of local variables.
Speaker
Andrew Kennedy is a software engineer at Facebook London working on the Hack team. Before joining Facebook in January this year he spent 16 years at Microsoft Research, during which time he helped design and implement the generics feature for the .NET Common Language Runtime and polymorphic units-of-measure inference for the F# programming language, in addition to making many research contributions in type systems, semantics, formal verification and compilation.
Lecture 15: The Rust Programming Language
This final APL topic addresses programming for memory safety, and in particular the techniques used in the Rust language. Rust is a fairly recent language, designed for “safe systems programming”: providing low-level precise control for programmers, minimal execution overheads, and promises about correct use of memory and threads. In this short introductory lecture I covered the basics of Rust, and gave a few small indications of how its C-like appearance masks a quite substantial effort to do things differently.
Continue reading Lecture 15: The Rust Programming Language
Lecture 14: Certifying Correctness
This afternoon’s lecture presented ways to take proofs of code properties beyond correctness or safety of specific code into the domain of mobile applications, guarantees of trustworthiness, and complete systems.
Continue reading Lecture 14: Certifying Correctness
Lecture 13: Practical Tools for Java Correctness
Today’s lecture presented two different facilities designed to help write Java code that does the right thing: the Java assert statement; and JML, the Java Modeling Language. Continue reading Lecture 13: Practical Tools for Java Correctness
Lecture 12: Specification and Verification
Today’s lecture was the first of three on language techniques and tools that aim to improve program correctness: not necessarily changing what a program does, the time or space it takes, or the power it uses; but making sure that what it does is the right thing to do. Of course, that also requires having some way to identify what that is to begin with.
Lecture 11: Cautionary Tales in Concurrency
This lecture concludes the set on concurrency with three distinctive challenges for concurrent programming and some possible solutions: lock networks, deadlock, and hand-over-hand locking; priority inversion in thread scheduling; and relaxed memory models for modern processor architectures. Continue reading Lecture 11: Cautionary Tales in Concurrency