Viewing profile — hiker

Plexes are first mentioned in 1960 https://dl.acm.org/doi/pdf/10.1145/366199.366256 and the paper even starts with a critique of the efficiency of Lisp's approach for representing …

Lean[1] Zulip chat[2] [1] https://leanprover-community.github.io/ [2] https://leanprover.zulipchat.com/

Liquid Tensor Experiment also comes to mind: https://www.nature.com/articles/d41586-021-01627-2 https://leanprover-community.github.io/blog/posts/lte-final/

Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment. [1] https://leanprover.zuli…

Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Has…

There are definitions for sheaves, Grothendieck topologies and sites[1] which were extensively used in the Liquid Tensor Experiment[2] [1] https://github.com/leanprover-community/m…

It still supports sbrk since it's available on WebAssembly but mmap is not. https://webassembly.org/docs/faq/#what-about-mmap

> Cool, I have no idea what the fuck this means and how it is useful to me. > Oh wait, I use them every day. Do you really? Do the `functions` you use even fit the above definition…

Lean[0]'s mathlib has quite nice formalisation of category theory[1] with plenty examples of concrete categories even sheaves and toposes. [0] https://leanprover.github.io/programm…

If the focus is on finite data structures only and the equivalence relation is "are the types isomorphic", then each type is isomorphic to the ordinary generating functor with some…

Maybe int getint(const char **s) { int res = 0; for (; **s && isspace(**s); (*s)++); for (; **s && isdigit(**s); (*s)++) res = 10 * res + **s - '0'; return res; }

Integer factorization is also reducible to Knapsack: To factorize integer N invoke a Knapsack solver with knapsack size of log(N) and items of size logarithm of all prime numbers u…

No suite of tests is complete enough to replace a proof. Unless the domain is finite and the tests exhaust all values in it.

> Data flow and perhaps control systems (AI scripts and GUIs built around something declarative and event-driven come to mind) indeed seem to be the only commercially successful ex…

Most typed languages have two separate levels: expressions (and statements in imperative languages) and types. Dependent types unify those two levels into one. This allows one to u…

"There are only two hard things in Computer Science: cache invalidation and naming things." -- Phil Karlton But I do like "Computability and naming things" better.

Going further one will need a word for "the kind of a kind", "the kind of a kind of a kind" and so on. One solution is TypeInType, that is the type of a type is another type (not k…

`Void` being the uninhabited type, in the light of the Curry-Howard isomorphism stands for a false proposition. `a -> Void` get interpreted as "not a" or "from a follows contradict…

> That's just not true. Functional programming does not eliminate state. And yet it says so in the first sentence in the Wikipedia page for functional programming https://en.wikipe…

Trees, graphs? Of course one can force anything into a relational database. The data analog of "Turing tarpit". Ironically graph databases are way better for describing relations t…

Except that functional programming completely eliminates (yet still allows) concern no. 1 in the mentioned order -- state > coupling > complexity > code. Not to mention the better …

I agree with everything besides your stated difficulties with infinities in type theory. Here's one infinity inductive ℕ : Type | zero : ℕ | succ (n : ℕ) : ℕ the type of natural nu…

Also set theory vs type theory (in Math) is really just dynamic typing vs static typing (in CS). And we already know how that played out in CS.

Not really. The boundaries of type theory (say HoTT) are exactly what is possible on a Turing machine (computable). And a step beyond those throws ZFC itself into paradoxes (say Ru…