Kutta

This is an unfortunate glaring false statement in the Morte documentation. Correctness of refactoring and code abstraction is understood to be with respect to semantic (extensional) equivalence, while normalization only works up to beta-eta equivalence. It can't eliminate abstraction in general.

Examples in Morte which suggest otherwise use hand-crafted forms of Church-encoded operations which are known to fuse, but there are many equivalent definitions which don't fuse, and which are actually more natural to write. Converting non-fusing definitions to fusing definitions is equivalent to supercompilation, which is generally undecidable, and thus can be implemented only up to some approximation.

I think this is an awful question with awful answers.

http://squid314.livejournal.com/323694.html

The Chernobyl reactor was very unsafe by modern standards, it did not have a containment vessel and tens of tons of reactor material was blown into the air, not a small amount.

This is always mentioned and I always fail to see the relevance. Inferable terms stay inferable when we add dependent types.

https://arxiv.org/abs/1610.01213

Section 3.2 of the paper absolutely does not say that the result does not hold. The main point of the construction is that typed quoted representations can preserve totality by disallowing diagonal application. Interpreting untyped quoted representations is impossible all the same, which is what I said in grandparent post.

I know Conor's views on total programming and share them, but the 2015 comment is not particularly relevant to the current topic, nor does it reflect on the folklore self-interpreter argument.

    f :: String -> ()
    f g' = case (eval g' :: Maybe (String -> ())) of
      Just g  -> g g'
      Nothing -> ()

    loop :: ()
    loop = f (quote f)

https://www.reddit.com/r/haskell/comments/3s93w1/a_selfinter...

To summarize, there are a number of different notions of self-interpretation. The strongest notion is interpreting from raw untyped syntax (which entails that the input is first type checked and some failing result is returned if it's invalid). This can be relatively easily proven to be impossible in any total language. The weakest notion of interpretation is the no-op embedding: quoted terms are terms themselves and self-interpretation is the identity function.

The weakest self-interpreter is trivial to implement but useless. The strongest one is very useful but impossible. The paper presents something which is weak enough to be possible but strong enough to be useful. It essentially Church encodes the terms of System F-omega as a fold over their structure. This makes it possible to implement pretty printers or structural equality. However, in this scheme all quoted terms are well-typed to begin with, also, quotation can not be invoked at runtime and is available through external preprocessing step only.

In this case, partial evaluation is a massively more principled and efficient way of doing metaprogramming than preprocessing or macros. There are limitations compared to Lisp-style unrestricted untyped metaprogramming, but not any that I would much miss in practice.

With partial evaluation, we automatically get type and scope safety, and also only need one language instead of several. Optimizations also cascade in a principled way: we can compile code-generating code to fast machine code, which we then use to generate faster code or generate it faster, but the then-resulting code can be also used to generate code, and so on.

On the more philosophical side, "philosophers should care about computational complexity", certainly, but it's not like one cannot have gradation in philosophical appeal. Also, it definitely helps to have computation at hand if we want to talk about feasible computation.

Remarkably, the four typing rules of equality suffice to generate all homotopical reasoning in classic HoTT. However, they aren't enough to prove univalence as a theorem, or at least no one knows how to do it. If we switch to cubical type theory, we get considerably more structure which allows us to prove univalence. But cubical type theory is also "synthetic" and builds up notions of spaces from ground-up.

In type theory every definable natural number is a program which evaluates to a concrete finite numeral. You can't get more grounded than that. Of course, there is still a large variety of standard and nonstandard models of type theory as well, but the computational interpretation already corresponds very closely to intuitions about intended (standard) models.

In contrast, the lack of clear computational meaning in classical theories makes it necessary find philosophical justifications, which in turn usually refer to other theories without clear computational meaning. Of course, we can compile classical proofs to programs as well through a variety of transformations, but they tend to be sort of unsatisfying, for example we may get functions with empty domains that we can't actually call, instead of programs evaluating to numerals.

So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers, rather statements referring to things which have properties which we think numbers should have. And then we can choose between sticking to first-order logic and leaving non-standard models in, or switching to second-order induction which lets us prove more statements at the cost of completeness and leaning more on ambient set theory.

Simpson seems to be critical of second-order logic because it's set theory in disguise; but to me that kind of dispute is moot because I find any sort of classical logic unsuitable for mathematical foundations.

I don't think is enough or appropriate. A significant fraction of global viewership is disturbed and alienated by the chants. It might well be that they're having the wrong feelings for wrong reasons, but realistically they will not adapt, and SpaceX's actions will not change their attitude in this regard, and they will continue to feel alienated.

I would like to see this properly weighted and considered as a consequence. It's similar to many other situations where you believe that people with different religions and attitudes are offended for ultimately wrong reasons, but you still don't go casually provoking them or making them feel bad.

http://lesswrong.com/lw/z0/the_pascals_wager_fallacy_fallacy...

Large payoff and small chance (with a wide confidence interval) has nothing to do with "infinite" payoff and "infinitesimal" chance. There are valid and interesting decision theoretic problems and paradoxes that arise with unbounded payoffs, but those aren't real-world in the way that outlier risk scenarios are real-world in banking and investment.

Cryonics is absolutely real-world in that sense, and we can and should hang some expected value tag there.

I have a fairly low confidence that cryonics will in fact work, but I wholly stand by my point that if it turns out to work, then that should be cause for a huge "we fucked up" moment coupled with a copious amount of soul-searching. But this shouldn't be put into a reference frame centered on "guilt" or "responsibility", although such things would be inevitably involved. Rather, it's a case of established models turning out to be wrong, and what matters is that everyone updates and learns from it as quickly as possible. Ignorance can be condoned but not willful and destructive ignorance in the face of ample evidence.