neel_k

This is a nice post! Jeremy Siek wrote a similar post a few years ago:

http://siek.blogspot.co.uk/2012/07/crash-course-on-notation-...

If I could add one thing to these two posts, it would be to learn Prolog.

We write inference rules top-down ("from these premises, we draw this conclusion"), but we often read them bottom-up ("given this goal, what facts could have lead to it?").

This double-vision thing, where you simultaneously view a set of inference rules in both a deductive and goal-directed fashion, is IMO one of the main stumbling blocks for people new to type theory. Luckily[1], however, it's fundamentally the same intuition that Prolog programmers develop -- and learning new programming languages is usually easy for programmers.

[1] It's not really by luck, of course: Prolog is called a logic programming language for a reason...

Total biomass actually peaked 540 million years ago, at the end of the Proterozoic era. See Figure 2 (on page 88) in Franck et al.: Causes and timing of future biosphere extinctions.

Link: https://www.biogeosciences.net/3/85/2006/bg-3-85-2006.pdf

Panini's grammar is closest to an instance of a Post canonical system. It is basically a set of general rewriting rules, with features going beyond BNF in power.

This is for pretty much the same reason that the grammatical formalisms modern linguists use also go beyond BNF. Linguists are interested in issues of grammaticality that actually do need context (such as subject-verb agreement) and so obviously context-free grammars can't do the whole job!

(For a programming example, you can see type correctness as a case of how well-formedness of programs depends on context -- whether a variable can be used in an expression depends on its type.)

That's interesting! I heard this from some CakeML people, who told me they decided to go with a full proof because it wasn't much more work for them. Maybe Compcert has a fancier register allocator architecture that benefits more from translation validation?

I haven't used Lean, but looking at its documentation, it supports universe polymorphism, very much like Agda. This means that there are countably many named universe levels, with each numbered universe containing the universe below it.

All of these numbered universes live inside of a top-most universe which contains all the types and universes. You can't quantify over the topmost universe, for exactly the same reason you can't form the set of all sets in ordinary set theory.

If you do pencil-and-paper mathematics particularly pedantically, when you define something like id, you will say you are working in Tarski-Grothendieck set theory, and then be careful to call it a "definition schema", rather than a "definition", because you are "really" giving a family of definitions, once for each Grothendieck universe. Distinguishing schemas and definitions is a little inconvenient on a computer -- the naive implementation forces you to implement everything twice -- and so one extra top universe is introduced as a home for all of the smaller universes. (Though Mizar apparently chooses to support universe-generic definitions, and to explain them to users as schemas.)

IME, these issues are generally ignorable, both on paper and on computers. Harper and Pollack gave an algorithm for inferring universe levels in the early 90s, and apparently it worked so well that they were worried their implementation was wrong (ie, would always say OK). So they carefully coded up various set-theoretic paradoxes in type theory and were relieved to discover their implementation rejected them.

HN seems to have eaten my first reply, so here's an abbreviated version.

It's easy to separate specification from verification with dependent types. You can (and I did) show students how to take ordinary simply-typed functional programs, give a specification as a different type, and then do a verification by producing a term of the appropriate specification type. Then, you can use this to motivate intrinsically-typed strategies, and (a) show the students that intrinsic/extrinsic is a gradient rather than a dichotomy, and (b) show them how to exploit this gradient systematically.

As for liveness, in a purely functional language, basically the only interesting liveness property is termination, and this didn't pose a challenge for the students. Indeed, it was the opposite -- I got a lot of questions about why Haskell lacked a termination checker. (They had in their minds that termination checking was an impossible dream, and so seeing a system with a termination checker that was both usable and useful really fired their imaginations.)

Specs were still hard. A proof-based approach is actually desirable for teaching good spec-writing skills, because proofs are more sensitive to the details of the spec. Eg, property-based testcase generation is happy with the equation that the reverse of the reverse of a list is the same list, but it's too weak an induction hypothesis for a proof. So it strongly motivates you to get to the characterizing equation for reversal (that reversing the concatenation of two lists is the concatenation of their reverses in the opposite order). (And it's still good for testcase generation.)

Unfortunately, I don't know enough small, self-contained examples where you have to strengthen the induction hypothesis to get the proof to go through. Ideally I'd want about 60 or 70 good examples of this (to set problems for a course) and, alas, I'd be hard-pressed to come up with a tenth that many satisfying examples.

> [...] even he had to take a few shortcuts in CompCert, e.g., he eschewed some termination proofs.

This turned out to be a premature optimization, actually! The CakeML compiler did full functional correctness proofs for their register allocator and report that it wasn't significantly harder than Compcert's translation validation.

> Writing a formal spec is no harder than writing tests (and arguably easier).

This, I'm much less sure of. IME, the really hard thing about correctness proofs is that specifications and proofs often require genuinely new ideas that didn't occur in the code.

For example, the spec of something like a sorting routine is that the output returns a list in increasing order, and that the output is a permutation of the input. The concept of a permutation doesn't occur explicitly in the implementation of the sort, and so the need to make this concept explicit can stop learners dead in their tracks.

I taught Agda (a dependently-typed programming language) to undergraduates, and found that Agda-the-programming language was actually easier to teach than Haskell (the IDE is better and there's less magic). But Agda-the-proof-assistant was hard to teach, mostly AFAICT because I don't know how to teach having mathematical ideas well.

> Teaching physics is a hard problem because there's a long and rich history of building upon previous advancements. You can't teach somebody quantum chromodynamics without first teaching them quantum electrodynamics, quantum mechanics, relativity, thermodynamics, classical mechanics, and all of the mathematical methods that come along with these.

I feel I was taught these things very inefficiently, though. Teaching tended to recapitulate the historical sequence in which the formalisms for each subject were developed, rather than developing the modern perspective from the outset. For example, Hamiltonians are typically taught in a final-year classical mechanics course (if they appear at all), but if they were taught early then statistical mechanics, electrodynamics and quantum mechanics would all be much easier. This even gives you a nice entry point to techniques for simulations via perturbative methods.

I'm not a physicist, though, so maybe there is some deep underlying reason for the way the curriculum is set up.

> And last time I tried typed racket I had some weird slow downs when specifying types less generally (like: integer instead of real, positive-integer instead of integer).

This is probably not your fault.

Scheme (from which Racket descends) has a very intricate numeric hierarchy. Typed Racket models the numeric hierarchy very accurately, and the technique they use to do this (intersection types) has bad worst-case complexity -- you can encode arbitrary SAT problems in it pretty easily. So the numeric types are actually aliases for quite complicated formulae, and this can tip you over into bad cases for inference. Writing a more specific type gives you a smaller formula, which makes typechecking faster.

In a clean-slate design, you would set things up to minimize the use of intersection types, but to get smooth access to the pre-existing Racket ecosystem, this is a price you have to pay.

(Warning: my information is a few years old. Racket's type system could have changed in the meantime.)

Yes, you're right. Thanks for the correction!

Probably the four most well-known pieces of software with end-to-end verification of functional correctness are the CertiKOS microkernel from Yale (verified in Coq), the SEL4 microkernel (verified in Isabelle), the Compcert C compiler (verified in Coq), the CakeML ML compiler (verified in Isabelle).

Stopping short of full end-to-end functional correctness, there are lot more notable examples, such as the Verve system at MSR (verified type/memory safety using Boogie), and the Bedrock system at MIT (functional correctness down to a fairly low-level IR, done in Coq), the miTLS/Everest TLS stack (protocol correctness verified in F-star, most of the way down to a C-like implementation), and the Iris project (a toolkit for verifying higher-order concurrent programs, currently being used to formalize Rust including unsafe, in Coq).

In machine-checked proof, the three biggest successes are the verification of the Odd Order Theorem (in Coq), the Four Colour Theorem (in Coq), and the Flyspeck project verifying the proof of the Kepler conjecture (in HOL).

In hardware verification, there has been a huge amount of work using ACL2 and HOL, but I don't know this space as well.

Basically, Coq and Isabelle have the most actual successes, but other things like F-star, Boogie and HOL have all worked as well.

This is basically the same thing I did, except that I worked as a programmer at a startup before going back to school for a PhD.

It was better than doing a startup by a stupidly huge margin. Startups are all about risk-minimization and risk-mitigation, since risky things mostly fail, and so use up your runway without moving you closer to success. So in a startup you are highly incentivized not to take big risks -- and research is always a risk. So you are driven to take an engineering mindset, where the apex of skill is to solve a new problem using only old, entirely proven techniques.

In contrast, after my first project as a PhD student, my advisor straight-up told me that I needed to shed the engineering mindset to succeed. Inventing new techniques was the goal, and so you need to adopt a mentality of confronting problems head on (rather than designing the system to avoid confronting them).

Basically a PhD puts you in an environment where you can take on big, poorly-understood and poorly-defined problems and attack them over and over again. Going from a blank sheet of paper to a solution (or clear failure) in six months 10 times over is an amazing way of improving your skills, and IME it's really hard to get this experience in industry (even though it's really valuable to have this experience in industry).

> I hear "dependent types" and I think "theorem prover", but it seems like Idris is a cleaned up Haskell with some light proving features built in?

It's a full-strength dependent type theory, but is intended primarily for use as a programming language. So the design focus is on using full dependent types to make ordinary programming easier.

> What's a good excuse to try Idris?

The best excuse of all: it is super fun.

Girard is French, and The Blind Spot is best understood as a piece of continental philosophy, not analytic.

The short version is that back in the late 60s, Althusser suggested that fields of knowledge inherently have "a blind spot" -- his idea was that every field of knowledge has to resort to structuring/organizational principles which cannot be properly articulated within the field of knowledge itself. Jacques-Alain Miller applied this idea to logic, arguing that the Fregean definition of equality (and hence number) exhibits precisely this kind of problem. Namely, Frege defined zero as the extension of the predicate "not equal to itself", and so Frege implicitly excludes the subject from logic, as Lacan had defined "subject" as the non-self-identical.

However, Alain Badiou objected very strongly against the extension of Althusser's ideas to logic. He thinks that science and mathematics can generate definitively true, objective, non-political knowledge, and so while blind spots can occur in daily ("ideological") life, they cannot occur in science.

Girard is essentially making an argument against Badiou and in favor of Miller. Because Girard is Girard, he never explicitly mentions any of these people in his lectures. This way, he can laugh at those of us who were too ill-informed to catch the fact that the TITLE of his lectures is a direct reference to Althusser.

Anyway, Girard begins with Lorenzen's idea that a proof can be understood as a dialogue between a proponent and a refuter, and the observation that the continuation-passing-style translation embedding classical logic into intuitionistic logic doesn't require that the answer type of the continuation be the empty type. He observes that these two ideas fit together in Krivine-style realizability models of classical logic: every formula can be interpreted as a set of proofs and refutations, and the interaction of a proof with a refutation yields a behaviour in the answer type. As a programmer, I think of the answer type as the runtime system of a programming language. The Krivine construction ensures that every proof -- every program -- both respects the invariants of the answer type/runtime system, and can never observe them.

So the runtime system of a programming language exhibits the essential structure of an Althusserian blind spot, and so via Curry-Howard so must logic.

I don't claim to understand the implications of all this, but I find the idea of bringing continental philosophy into the foundations of logic in a really serious, technically profitable way to be very exciting.

I'm more on the theory end of PL, but in my experience program committees generally regard difficulty as a negative for a paper. The main thing PCs want is for papers which make progress on important problems. Now, you can do this either by (1) attacking existing open problems, or (2) by finding new important problems.

It's easy to tell that a long-standing open problem is important, but generally these problems are open because they are hard, and consequently the technical sophistication for new attacks on them is generally very high.[] New problems can often be solved with relatively simple techniques, but it's also difficult to tell if a new problem is genuinely important or just some random thing made up for submission.

With a low acceptance rate, PCs tend to favor type (1) papers over type (2) papers, because few people feel comfortable arguing for a paper that might* be doing something important over one that is doing something important. This is widely seen as a failure mode of low acceptance-rate venues.

So over the last several years many of the top PL conferences (such as POPL, LICS and PLDI) have moved to a multiple track format in order to increase the number of papers they accept. This is precisely to give program committees the freedom to take chances on "risky" papers that might become important, or might become footnotes.

[*] Occasionally, someone will solve a difficult open problem with simple techniques, and these papers are immediately accepted with much rejoicing. It's easy to have your cake and eat it, when you have two cakes...

You almost certainly have had to debug a Gödelian paradox in your day-to-day programming. It's just that programmers call it "nontermination" or "infinite loops".

In 1952 the logician Martin Löb invented something called "provability logic" as a way to formulate Gödel's theorem more abstractly, so that we could see how the proof worked without having to work with explicit numerical encodings of formulas. (Think of this as the difference between working with strings versus abstract syntax trees.)

His version of the proof is now called Löb's theorem, and its structure is almost identical to what logicians call Curry's paradox, and which (via the Curry-Howard correspondence) programmers know as the Y combinator. The Y combinator is used to implement recursion in the lambda calculus, specifically including the ability to go into infinite loops.

I blogged about this last year:

http://semantic-domain.blogspot.co.uk/2016/05/lobs-theorem-i...

That's pretty accurate! (I'm one of the authors.)

In event-based programming, one of the basic abstractions are something variously called "events", "futures", or "promises". The idea of a future is that it is a data structure that can yield a value at some point in the future, but not might be ready to produce one right away. This idea dates back to (at least) MultiLisp and the Connection Machine, but many modern languages support this primitive -- for example, Javascript, Rust, Ocaml, C#, Java and Scala all have good library support for it.

Our basic idea is that futures correspond very closely to the interpretation of the "eventually" operator in temporal logic. So if we could give a typed lambda calculus for temporal logic, then we could implement the eventually operator with futures. The benefit of doing this is that we could design languages which combine the easiness of reasoning featured by purely functional programming, while still offering good support for event-based programming (eg, for GUIs). In addition, if we are coming from a typed language that has enough invariants, we can also simplify the implementation of futures (since we know statically that certain problems like deadlock can't arise).

My personal goal is to figure out the fundamental primitives of interactive programming. Ultimately I'd like to be able to go from a framebuffer to a comfortable GUI toolkit in a few hundred lines of code, so that teaching the principles of how to implement these things can fit into a semester-long course. (Since there is a fairly small limit on how much code a student can reasonably write/comprehend in a term, the better we understand a problem the more we can teach.)