Royal Navy whistleblower says Trident is "a disaster waiting to happen"

A Royal Navy weapons expert who served on HMS Victorious from January to April this year has released via WikiLeaks an eighteen-page report claiming Trident is "a disaster waiting to happen".

McNeil's report on WikiLeaks.

Original report in The Sunday Herald.

McNeilly's report alleges 30 safety and security flaws on Trident submarines, based at Faslane on the Clyde. They include failures in testing whether missiles could be safely launched, burning toilet rolls starting a fire in a missile compartment, and security passes and bags going unchecked.
He also reports alarms being muted because they went off so often, missile safety procedures being ignored and top secret information left unguarded.

The independent nuclear submarine expert, John Large, concluded McNeilly was credible, though he may have misunderstood some of the things he saw.
Large said: "Even if he is right about the disorganisation, lack of morale, and sheer foolhardiness of the personnel around him - and the unreliability of the engineered systems - it is likely that the Trident system as a whole will tolerate the misdemeanours, as it's designed to do." 

(Regarding the quote from Large, I'm less sanguine. Ignoring alarms is a standard prelude to disaster. See Normal Accidents.)

Second report in The National.

“We are so close to a nuclear disaster it is shocking, and yet everybody is accepting the risk to the public,” he warned. “It’s just a matter of time before we’re infiltrated by a psychopath or a terrorist.”

Coverage in CommonSpace.

Summer School on DSL Design and Implementation

The Scala team at EPFL is running a Summer School on DSL Design and Implementation, 12-17 July in Lausanne, Switzerland. They have a great line-up, including Martin Odersky, Tiark Rompf, Kunle Olukotun, and Matthew Flatt. I'll be there, speaking on A practical theory of language-integrated query and Quoted Domain Specific Languages: Everything old is new again.

Status Report 5

I am recovered. My bone marrow biopsy and my scan at the National Amyloidosis Centre show no problems, and my urologist has discharged me. Photo above shows me and Bob Harper (otherwise known as TSOPLRWOKE, The Society of Programming Language Researchers With One Kidney Each) at Asilomar for Snapl.

My thanks again to staff of the NHS. Everyone was uniformly friendly and professional, and the standard of care has been excellent. My thanks also to everyone who wished me well, and especially to the SIGPLAN EC, who passed a get-well card around the world for signing, as shown below. I am touched to have received so many good wishes.

Related: Status Report, Status Report 2, A paean to the Western General, Status Report 3, Status Report 4.

Bright Club: Computability

A brief introduction to the hilarious subject of computability theory. Performed as part of Bright Club at The Stand in Edinburgh, on Tuesday 28 April 2015.

Fractal Maps

Sky Welch's Fractal Maps updates Alasdair Corbett's Mandelbrot Maps. It renders faster, and displays the two curves side-by-side (rather than displaying one large and one tiny). Mandelbrot Maps is the most popular Mandelbrot app in Google Play, with over 10,000 downloads. I expect Fractal Maps to catch up soon. Try it today! (Disclaimer/boast: both Sky and Alasdair produced their software as part of UG4 projects under my supervision.)

Bright Club

I'm performing at Bright Club, Edinburgh, Tuesday 28 April at The Stand. Doors open 7:30, show begins 8:30. See you there! Details, tickets £5.

Prime Minister of Singapore plans to learn Haskell

The Prime Minister of Singapore, Lee Hsien Loong, plans to learn Haskell.

My children are in IT, two of them – both graduated from MIT. One of them browsed a book and said, “Here, read this”. It said “Haskell – learn you a Haskell for great good”, and one day that will be my retirement reading.

Spotted by Jeremy Yallop.

Multiple inheritance, revisited

Via @ReifyReflect (Sam Lindley) and @PedalKings. Previously: Multiple inheritance.

A complement to blame

A complement to blame
Philip Wadler.
SNAPL, May 2015.

Contracts, gradual typing, and hybrid typing all permit less-precisely typed and more-precisely typed code to interact. Blame calculus encompasses these, and guarantees blame safety: blame for type errors always lays with less-precisely typed code. This paper serves as a complement to the literature on blame calculus: it elaborates on motivation, comments on the reception of the work, critiques some work for not properly attending to blame, and looks forward to applications. No knowledge of contracts, gradual typing, hybrid typing, or blame calculus is assumed.

Blame and Coercion:Together Again for the First Time

Blame and Coercion:Together Again for the First Time
Jeremy Siek, Peter Thiemann, Philip Wadler.
PLDI, June 2015.

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop three calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are: λB, based on the blame calculus of Wadler and Findler (2009); λC, inspired by the coercion calculus of Henglein (1994); λS inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006) and the threesome calculus of Siek and Wadler (2010). While λB is little changed from previous work, λC and λS are new. Together, λB, λC, and λS provide a coherent foundation for design, implementation, and optimisation of gradual types.

We define translations from λB to λC and from λC to λS. Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: λC has a particularly simple definition, and the subtle definition of blame safety for λB is justified by the simple definition of blame safety for λC. Our calculus λS is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from λC to λS to validate the challenging part of full abstraction between λB and λC; and, second, using full abstraction from λB to λS to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.