Lambda the Ultimate

The Experimental Effectiveness of Mathematical Proof

The aim of this paper is twofold. First, it is an attempt to give an answer to the famous essay of Eugene Wigner about the unreasonable effectiveness of mathematics in the natural sciences [25]. We will argue that mathematics are not only reasonably effective, but that they are also objectively effective in a sense that can be given a precise meaning. For that—and this is the second aim of this paper—we shall reconsider some aspects of Popper’s epistemology [23] in the light of recent advances of proof theory [8, 20], in order to clarify the interaction between pure mathematical reasoning (in the sense of a formal system) and the use of empirical hypotheses (in the sense of the natural sciences).

The technical contribution of this paper is the proof-theoretic analysis of the problem (already evoked in [23]) of the experimental modus tollens, that deals with the combination of a formal proof of the implication U ⇒ V with an experimental falsification of V to get an experimental falsification of U in the case where the formulæ U and V express empirical theories in a sense close to Popper’s. We propose a practical solution to this problem based on Krivine’s theory of classical realizability [20], and describe a simple procedure to extract from a formal proof of U ⇒ V (formalized in classical second-order arithmetic) and a falsifying instance of V a computer program that performs a finite sequence of tests on the empirical theory U until it finds (in finite time) a falsifying instance of U.

I thought I had already posted this, but apparently not.

Consider this paper the main gauntlet thrown down to those who insist that mathematical logic, the Curry-Howard Isomorphism, etc. might be fine for "algorithmic code" (as if there were any other kind) but is somehow inapplicable the moment a system interacts with the "real" or "outside" world (as if software weren't real).

Update: the author is Alexandre Miquel, and the citation is "Chapitre du livre Anachronismes logiques, à paraître dans la collection Logique, Langage, Sciences, Philosophie, aux Publications de la Sorbonne. Éd.: Myriam Quatrini et Samuel Tronçon, 2010."

Microsoft has recently detailed their "Compiler as a Service" initiative in a whitepaper. The whitepaper calls the project Roslyn.

Related, IBM sponsors the Eclipse IMP project for its X10 language (and the X10DT). IMP is also used for Eelco Visser's Spoofax IDE and WebDSL IDE.

It is being reported that John McCarthy has passed. Here is an example article which I list only for confirmation of something I heard from a friend.

John McCarthy, the creator of the Lisp programming language and a pioneer in artificial intelligence, has died. He was 84.

I hope that LtU'ers will comment appropriately.

My personal and very indirect remembrance is quite simple: In the late 1980s, as a high school student fascinated by computers but with only limited access to any and with even more limited access to education about them -- I went trolling what bookstores I could find that might have something to offer. I was not rich but I could afford a few bucks to take a commuter train 40 miles to Boston. Once in Boston, I learned how to navigate to Cambridge, near Harvard. Once there I found the Harvard Coop. Once at the Coop I learned where to find textbooks. And there, very early on in my experience with computing, I found a reprint of the Lisp 1.5 manual. I recognized it as "dated" (even then) very quickly but I also was blown away by the presentation of (more or less) a meta-circular eval. The handling of m- vs. s-expressions also demystified for my then quite naive, unworldly self a lot about the nonthreatening, practical, and banal nature of many notational choices. I don't know... I'm certainly not the right person to sing the man's praises other than to say that his work touched my life in a big positive way that is hard to sum up.

I have just learned that Dennis Ritchie (1941-2011) has passed away. His contributions changed the computing world. As everyone here knows, dmr developed C, and with Brian Kernighan co-authored K&R, a book that served many of us in school and in our professional lives and remains a classic text in the field, if only for its style and elegance. He was also one of the central figures behind UNIX. Major programming languages, notably C++ and Java, are descendants of Ritchie's work; many other programming languages in use today show traces of his influences.

Update

Bjarne Stroustrup puts the C revolution in perspective: They said it couldn’t be done, and he did it.

A while back we learned about Google's thoughts on Javascript. Well, it seems Google's Dart Language is now live.

Dart is a new class-based programming language for creating structured web applications. Developed with the goals of simplicity, efficiency, and scalability, the Dart language combines powerful new language features with familiar language constructs into a clear, readable syntax.

The full specification (PDF)

A feature I find interesting is that you can add static types:

Dart programmers can optionally add static types to their code. Depending on programmer preference and stage of application development, the code can migrate from a simple, untyped experimental prototype to a complex, modular application with typing. Because types state programmer intent, less documentation is required to explain what is happening in the code, and type-checking tools can be used for debugging.

this will improve reliability and maintainability, I imagine, right?

Steve Jobs (1955 - 2011) had a profound influence on the computing world. As others discuss his many contributions and accomplishments, I think it is appropriate that we discuss how these affected programming, and consequently programming languages. Bringing to life some of the ideas of the Mother of All Demos, Jobs had a hand in making event loops standard programming fare, and was there when Apple and NeXT pushed languages such as Objective-C and Dylan and various software frameworks, and decided to cease supporting others. Some of these were more successful than others, and I am sure members have views on their technical merits. This thread is for discussing Jobs -- from the perspective of programming languages and technologies.

Update:

Eric Schmidt on Jobs and OOP

Stephen Wolfram on Jobs and Mathematica

The iPhone mandate decision

Given successes in parallel frameworks for linear algebra (BLAS) and log processing (MapReduce), the current trend in large scale data parallelism seems to be more general graph processing. An early big contender discussed here was Google's Pregel.

Two fun ones have been making the rounds. First, and fairly related, is GraphLab:

Designing and implementing efficient, provably correct parallel machine learning (ML) algorithms is challenging. Existing high-level parallel abstractions like MapReduce are insufficiently expressive while low-level tools like MPI and Pthreads leave ML experts repeatedly solving the same design challenges. By targeting common patterns in ML, we developed GraphLab, which improves upon abstractions like MapReduce by compactly expressing asynchronous iterative algorithms with sparse computational dependencies while ensuring data consistency and achieving a high degree of parallel performance. We demonstrate the expressiveness of the GraphLab framework by designing and implementing parallel versions of belief propagation, Gibbs sampling, Co-EM, Lasso and Compressed Sensing. We show that using GraphLab we can achieve excellent parallel performance on large scale real-world problems.

There are obvious connections to systems like Cilk/TBB and, more focused on graphs, Pingali's Amorphous Data Parallelism work.

A radically different approach is John Gilbert's Parallel Combinatorial BLAS: A Toolbox for High-Performance Graph Computation (papers, slides):

This paper presents a scalable high-performance software library to be used for graph analysis and data mining. Large combinatorial graphs appear in many applications of high-performance computing, including computational biology, informatics, analytics, web search, dynamical systems, and sparse matrix methods. Graph computations are difficult to parallelize using traditional approaches due to their irregular nature and low operational intensity. Many graph computations, however, contain sufficient coarse grained parallelism for thousands of processors, which can be uncovered by using the right primitives.

We describe the Parallel Combinatorial BLAS, which consists of a small but powerful set of linear algebra primitives specifically targeting graph and data mining applications. We provide an extendible library interface and some guiding principles for future development. The library is evaluated using two important graph algorithms, in terms of both performance and ease-of- use. The scalability and raw performance of the example applications, using the combinatorial BLAS, are unprecedented on distributed memory clusters.

The approach to performance in both is fairly different. Intriguing to me is the choices in frontend languages: given the constrained domains, I suspect much higher level languages are possible (hint: synthesis).

Note: Saw this on Sunday (9/11), but waited for it to go viral before posting it here.

A leaked Google memo, The Future of JavaScript, from November 2010 is being circulated around the Internet, outlining Google's supposed technical strategy for Web programming languages. Google plans to improve JavaScript, while also creating a competitor to JavaScript, Dart (ex-Dash), that it hopes will be the new lingua franca of the Web.

Ironically, I saw this leak via a Google Alert keyword search. It has propagated to at least Github, the Dzone social network, The Register and Information Week since Sunday.

A. Dehon, B. Karel, B. Montagu, B. Pierce, J. Smith, T. Knight, S. Ray, G. Sullivan, G. Malecha, G. Morrisett, R. Pollack, R. Morisset & O. Shivers. Preliminary design of the SAFE platform. In Proceedings of the 6th Workshop on Programming Languages and Operating Systems (PLOS 2011). ACM, Oct. 2011.

ABSTRACT — Safe is a clean-slate design for a secure host architecture, coupling advances in programming languages, operating systems, and hardware, and incorporating formal methods at every step. The project is still at an early stage, but we have identified a set of fundamental architectural choices that we believe will work together to yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.

Proving an operating system correct down to the hardware specification and against a threat model does seem to demand new programming languages and higher-order constructive type theory.

Nick Benton and Neel Krishnaswami, ICFP'11, A Semantic Model for Graphical User Interfaces:

We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. [..] We capture the arbitrariness of user input [..] [by a nondeterminism] “powerspace” monad.

Algebras for the powerspace monad yield a model of intuitionistic linear logic, which we exploit in the definition of a mixed linear/non-linear domain-specific language for writing GUI programs. The non-linear part of the language is used for writing reactive stream-processing functions whilst the linear sublanguage naturally captures the generativity and usage constraints on the various linear objects in GUIs, such as the elements of a DOM or scene graph.

We have implemented this DSL as an extension to OCaml, and give examples demonstrating that programs in this style can be short and readable.

This is an application of their (more squiggly) LICS'11 submission, Ultrametric Semantics of Reactive Programs. In both these cases, I find appealing the fact the semantic model led to a type system and a language that was tricky to find.