neel_k

10 ms·

31.
by neel_k 6y ago
Most likely it will do the opposite. Losing a year of revenue will straight up kill a bunch of universities, just like it would kill most businesses. However, the following year there will still be the same number of 18 year olds who want t
32.
by neel_k 6y ago
TeXmacs is a marvel, and for literally decades I've wondered why it hasn't seen broader adoption.
33.
by neel_k 7y ago
Both go and OCaml use LR parser generators, precisely because they make it easy to give excellent error messages. Basically the key insight is that you can use the parsing automaton state to classify syntax errors, which makes it as easy as
34.
by neel_k 7y ago
Basic blocks with arguments is purely an alternate syntax for SSA. From a teaching perspective, I like blocks-with-arguments a lot better, since it lets students reuse their intuitions about tail-calling functions. However, there's no
35.
by neel_k 7y ago
In modern terms, you can identify sequences and automata: a sequence is a current state, plus a transition function giving you the next element of the sequence and the next state. However, if every function is tracked by a computable proc
36.
by neel_k 7y ago
You are being a bit too quick to equate finitism and constructivism. Hilbert was a finitist, but not a constructivist, and Brouwer was a constructivist, but he was not a finitist. Brouwer's analysis of the continuum depends heavily upo
37.
by neel_k 7y ago
Brouwer was absolutely not a finitist! Indeed, he completely rejected the idea that you could use formal logic to bound what mathematics could talk about. A better (but still not entirely accurate) description would be that Brouwer had an e
38.
by neel_k 7y ago
I think lifetimes and lvalues are both reasonably straightforward to understand in terms of linear logic. IMO, the main difficulty with adding monad-like abstractions to Rust actually lies elsewhere, in the fact that Rust doesn't reall
39.
by neel_k 7y ago
It's actually super easy to achieve in general: literally (and I genuinely mean literally) tens of thousands of primary schools manage it. You need (a) the members of the culture to have a shared ethos that sees the work as a noble pur
40.
by neel_k 7y ago
Actually, there is a critically bad interaction between the way that garbage collection algorithms work and the LRU heuristic for swap. Tracing garbage collection algorithms work by doing a graph traversal that traces all the live pointers
41.
by neel_k 7y ago
It's taking on a fair amount of risk to use a language that (a) encourages the use of concurrency but (b) is not memory-safe when you do so, especially when writing network-facing code. Go uses multi-word primitive values, which means
42.
by neel_k 7y ago
> The only difference is that for some reason they dive right into esoteric definitions like "monoids" and "magmas" and "monads" instead of the bedrock useful things from algebra like "groups", &qu
43.
by neel_k 7y ago
I half-agree with you. The agreement part is that the algebraic structures that naturally arise in my programming experience are indeed ultra-basic: monoids, lattices, semirings, partial orders, and so on. (When I need elementary linear alg
44.
by neel_k 7y ago
The founding act of denotational semantics was Scott's model of the untyped lambda calculus, which is surely the paradigmatic dynamically typed language. Moreover, its creation led to an immense body of work on type theory, because the
45.
by neel_k 7y ago
The "normal" physical systems we build (say houses and hydraulic systems) are mostly "continuous". This means small changes in the inputs generally result in small changes in the behaviour of the system. So, for exampl
46.
by neel_k 7y ago
It may be professional deformation speaking, but they seem to be using "applied category theory" in a coherent and natural sense: they mean the theory of monoidal categories, (a) viewed as a generalization of linear algebra, and (
47.
by neel_k 8y ago
> That's what the author called "alt" and I don't understand why the author objects to it. His "neutral pseudocode" is Go, which lacks good support for parameterized types. As a result there would be quite a
48.
by neel_k 8y ago
Semantically, returning a sum type like Result<T,E> absolutely is the same thing as exceptions (ie, it's the exception monad). However, there's one very important language design difference between this and Java-styled check
49.
by neel_k 8y ago
No. From an implementation POV, Prolog adds two pieces to ordinary programming languages: backtracking plus unification. This post talks about backtracking, but doesn't touch upon unification at all.
50.
by neel_k 8y ago
Eleven years on, this remains one of my favorite papers! There's a pretty variant of this idea introduced in 1995 by Valentin Antimirov called partial derivatives of regular expressions. His idea was to replace the single derivative
51.
by neel_k 8y ago
Hello, You can see the current version of the class at: https://www.cl.cam.ac.uk/teaching/1819/ProgC I've moved to a style where the lectures are recorded and the lecture hours have been replaced with lab ses
52.
by neel_k 8y ago
The literature on this subject is both vast and populated by the work of the most eminent philosophers -- both continental and analytic -- of the last two hundred years. Here are some books that I liked. However, there are three caveats. Fi
53.
by neel_k 8y ago
Grad students are actually more expensive, because they're slower and more likely to mess up than a pro would. However, you still want the grad students to do it. A successful experimental physicist needs to have a deep feeling for how
54.
by neel_k 8y ago
Yes, the UK government is behind the erosion of free speech on campus. The Counter Terrorism and Security Act of 2015 imposes a statutory duty on universities to have a "due regard to the need to prevent individuals from being drawn in
55.
by neel_k 9y ago
Making parsing easily incrementalizable is a valuable property, because gramars which incrementalize easily also localize parse errors well, and having both of these properties hold lets you offer convenient APIs for IDEs and text editors m
56.
by neel_k 9y ago
> Are models of observational type theory exactly elementary toposes? By design, the answer is no. Toposes are models of intuitionistic bounded ZF. However, in general dependent type theories, including observational type theory, don&#x2
57.
by neel_k 9y ago
Oh, wow -- thanks especially for that second link! I was wondering about this recently.
58.
by neel_k 9y ago
I should add that Gordon Plotkin gave a keynote at POPL this year, Some Principles of Differentiable Programming , where he discusses this from the angle of probabilistic programming. It's on Youtube at: https://www.youtube
59.
by neel_k 9y ago
At a super high level, the central problem is higher-order functions. If you have a programming language, you can think of differentiation as being a higher-order function that takes a function a and returns a new function as a result. If y
60.
by neel_k 9y ago
> Also, does anyone know if what he refers to as "progress and preservation" are the same / related to "liveness and safety" in distributed algorithms? It sounds like the same kind of idea. Progress and preservat

More ›