Viewing profile — Kutta

It will release approximately no CO2.

The "small amounts is cardioprotective" is most likely false, the new recommendation simply reflects this. I recall reading about this in research more than 10 years ago. (Sorry fo…

Yes, the point is that the user only has to write an interpreter, not a compiler, the compiler is automatically generated. See also GraalVM's Truffle interpreter or Souffle Datalog…

Futamura projection is an entirely standard concept in staged compilation. The hand-wringing is unwarranted.

I would also guess they don't give a fuck about the night sky either.

Are you literally not aware that all pieces of internet infrastructure currently in use have to be replaced every N years?

Arenas have been used in Rust for a long time.

> We already have a perfectly good foundation of mathematics. It's called ZFC [1] This is completely missing a core point of category theory and type theory (which is about categor…

What you say is kind of interesting but I get the impression that we are talking past each other. id(X): ==(X, rec_0(0, X)) Sorry, what's this supposed mean, is it a definition? Th…

A type system cannot be TC. What you seem to talk about, is that if a type checker can simulate arbitrary TM's through an encoding of its input, then the type checker is necessaril…

I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way. ZFC and MLTT do not differ in that decidability of pro…

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to check…

OpenAI should have never been open, named "OpenAI", or advertised itself as being open. At the time of OpenAI's inception, much of the AI risk community deemed it as harmful, altho…

This tutorial seems to miss the level-based generalization optimization, which is crucial for production-strength HM inference. For, that you can look at: http://okmij.org/ftp/ML/g…

I also recommend Nick Bostrom's article "The Future of Human Evolution", predating OP by ten years, which contains essentially the same arguments and conclusions. https://www.nickb…

Usually it's not possible to form such a predicate. If we have impredicative base universe, then it's possible to form a predicate over all types in the base universe (which may or…

Absolutely fucking no.

The human spaceflight ability of NASA trended sharply to zero in the last 50 years, with space travel getting more expensive, more dangerous and far less capable than before, going…

Immutability is an implementation detail with no inherent value. What we actually care about is referential transparency, encapsulation & tracking of effects, performance, abstract…

I thought the cost of GC following a pointer into a compact region is basically constant time, or is that incorrect?

I agree that storing a reference besides an Entry is probably safer than #touch. It's also similar to arrays slices, where we store reference to the array itself + offsets. The ST-…

You need something which decreases on each step. You could try to recurse on the number of unvisited nodes in the graph. You can try well-founded recursion if this does not work fo…

Awful comment. The OP, while not pedagogically ideal, demonstrates proof writing along the Curry-Howard correspondence, an extremely deep topic which predates popular functional pr…