Onward! 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
co-located with SPLASH 2016
Wed 2 Nov 2016 13:30 - 14:20 at Zürich 2 - Onward! Essays I

Functional languages with strong static type systems have beneficial properties to help ensure program correctness and reliability. Surprisingly, their practical significance in applications is low relative to other languages lacking in those dimensions. In this paper, the programs-as-proofs analogy is taken seriously to gain speculative insights by analysis of creation habits in the proof-centric discipline of mathematics. Viewed in light of this analogy, a sampling of mathematicians’ attitudes towards formal proof suggests that the crucial role of intuition and experimentation in programming tasks may be under appreciated, hinting at a possible explanation of the challenges rigorously disciplined languages face in practical applications.

Slides: How Are Programs Found? (how-are-programs-found-slides.pdf)6.94MiB

Wed 2 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:10
Onward! Essays IOnward! Essays at Zürich 2
How Are Programs Found? Speculating about Language Ergonomics with Curry-Howard
Onward! Essays
DOI Pre-print File Attached
The Left Hand of Equals
Onward! Essays
James Noble Victoria University of Wellington, New Zealand, Andrew Black Portland State University, Kim Bruce Pomona College, Michael Homer Victoria University of Wellington, Mark Miller Google Inc.