Recursion in R

I've been (trying to) learn a little about R, mostly in self-defense because I'm involved in a project with others using it.

R has lots of fun features, such as built-in support for vector and matrix operations and overloading, which make it well-suited to its domain, statistical programming and modeling.

However, there are also some things that are just plain weird, at least from the point of view of programming language design.  Scoping and lazy evaluation interact in a subtle way,  particularly with regard to recursion.

ETA: JavaScript does exactly the same thing. Yech.
ETA2: And Python. Sigh.

Read more »

How to publish research accompanied by mechanically-checkable proofs

I've both written and reviewed research papers that incorporate mechanically-checked proofs (either as the main subject of the research or as supporting the correctness of other contributions).  Computer-aided formalization and proof are increasingly part of the mainstream of (the formal side of) programming languages research, and seem to be being especially enthusiastically adopted by students and junior researchers.  However, just having mechanically verified a proof of (some aspect of) a system is not enough - all of the standard considerations regarding the reporting of scientific research, on-paper proofs, or research code still apply. 

This post collects some guidelines that I hope will be helpful for researchers working on papers accompanied by formal proofs. I would have thought most of these were obvious, but have encountered enough counterexamples to disabuse me of this naive assumption.  The following is probably not an exhaustive list, but is offered as a starting point.


Read more »