neel_k

16 ms·

61.
by neel_k 9y ago
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 w
62.
by neel_k 9y ago
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&#x
63.
by neel_k 9y ago
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 m
64.
by neel_k 9y ago
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
65.
by neel_k 9y ago
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
66.
by neel_k 9y ago
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 pr
67.
by neel_k 9y ago
> [...] 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 a
68.
by neel_k 9y ago
> 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 m
69.
by neel_k 9y ago
> 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 descen
70.
by neel_k 9y ago
Yes, you're right. Thanks for the correction!
71.
by neel_k 9y ago
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 (veri
72.
by neel_k 9y ago
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
73.
by neel_k 9y ago
> 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 prim
74.
by neel_k 9y ago
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&quot
75.
by neel_k 10y ago
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 eith
76.
by neel_k 10y ago
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 c
77.
by neel_k 10y ago
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 t