Footpost

Well since Neuromorphic methods can show that 138240 = 0, should it come as as surprise that they enable blockchain on Mars?

https://cointelegraph.com/news/neuromorphic-computing-breakt...

Neuromorphic computation has been hyped up for ~ 20 year by now. So far it has dramatically underperformed, at least vis-a-vis the hype.

The article does not distinguish between training and inference. Google Edge TPUs https://coral.ai/products/ each one is capable of performing 4 trillion operations per second (4 TOPS), using 2 watts of power—that's 2 TOPS per watt. So inference is already cheaper than the 20 watts the paper attributes to the brain. To be sure, LLM training is expensive, but so is raising a child for 20 years. Unlike the child, LLMs can share weights, and amortise the energy cost of training.

Another core problem with neuromorphic computation is that we currently have no meaningful idea how the brain produces intelligence, so it seems to be a bit premature to claim we can copy this mechanism. Here is what the Nvidia Chief Scientist B. Dally (and one of the main developers of modern GPU architectures) says about the subject: "I keep getting those calls from those people who claim they are doing neuromorphic computing and they claim there is something magical about it because it's the way that the brain works ... but it's truly more like building an airplane by putting feathers on it and flapping with the wings!" From "Hardware for Deep Learning" HotChips 2023 keynote. https://www.youtube.com/watch?v=rsxCZAE8QNA This is at 21:28. The whole talk is brilliant and worth watching.

The reasoning for this choice in the base ISA is discussed in the RISCV ISA manual, Section 2.4 on "Integer Computational Instructions" [1]. Given that RISCV is a modular ISA, it should be possible in principle to have suitable ISA extensions that do integer overflow detection. Maybe the absence of such an extension in 2025 indicates that this is not a pressing need for many RISC-V users?

[1] https://lists.riscv.org/g/tech-unprivileged/attachment/535/0...

Andy Pitts' writing is extremely clear, whatever he writes about. This clarity is not easy to achieve and shows mastery!

The full abstraction for PCF was solved in the mid 1990s by Abramsky/Jagadeesan/Malacaria [1] Hyland/Ong [2] and Nickau [3]. All three appeared simultaneously. This was a paradigm shift, because all three used used interactive rather than functional models of computation. (There was also later work on domain theoretic full abstraction, e.g. OHearn and Riecke [4], but I can't recall details. Maybe Streicher's work was in this direction?) The beauty of interative models like games is that they can naturally encode more complex behaviour, including parallelism.

[1] S. Abramsky, R. Jagadeesan, P. Malacaria, Full Abstraction for PCF.

[2] J.M. E. Hyland, C.-H. L. Ong, On Full Abstraction for PCF: I, II, and III.

[3] H. Nickau, Hereditarily sequential functionals.

[4] P. O'Hearn, J. G. Riecke, Kripke logical relations and PCF.

Domain theory has reduced to a trickle, with almost no new results since the late 1990s. Most domain theorist have retired, or moved on to other things. Aside, Andy Pitts has been made a fellow of the Royal Society a few days ago!

That's interesting. What would you teach in the language design part of the course? By the time compilers are taught (2nd or 3rd year undergraduate), most students rarely understand advanced language concepts, whether call/cc, GADTs, higher-kinded types, or type-based lifetime tracking, message-passing vs shared memory parallelism etc, let alone the tradeoffs involved in the design space.

Note also that there is no scientific consensus on what makes for a good programming language.

The great G.-C. Rota quipped:

   Probability theory = combinatorics divided by n 

In this vein let me add:

   Information theory = log(probability theory)

   practical DSLs

Isn't embedding a "practical DSLs" another toy compiler?

Except that with a DSL, you have to worry about gnarly but not-so-interesting problems like what happens to my syntax (given by a CFG) when I add another syntax (another CFG)? Are the combined CFGs ambiguous etc?

Keep things simple!

The main conceptual novelty that modern machine learning brings is the addition of computational complexity in the mix: from information theory's question

   what is learnable?

to

   what is learnable in
   poly-time?

(or similar resource constraints). This was pioneered, as far as I am aware, in Valiant's A Theory of the Learnable (please correct me if I'm wrong, I'm not an ML/AI historian). Interestingly, we see a similar evolution of Shannon's thinking about cryptography (what is secure information theoretically, i.e. against computationally unbounded adversaries?) to: what is safe against a poly-time restricted adversary?

That's interesting. I certainly did not make the Reddit post. Since there is interest in proto-GANs, here are two more.

- J. Schmidhuber, Learning Factorial Codes By Predictability Minimization. (1992)

- W. Li, M. Gauci, R. Gross, A Coevolutionary Approach to Learn Animal Behavior Through Controlled Interaction. (2013)

Schmidhuber's work will be widely known (and its relationship with GANs controversial), but I can't recall where I read about Li et al.

   Co-evolving parasites

This paper strikes me as the earliest manifestation of what would later become GANs (generative adversarial networks). Yes, the mechanism is different (GAs vs NNs), but the spirit (having a competitive mechanism for speeding up local search) is similar.

They are not mutually exclusive:

- Use HoTT or any other type theory as a logic / foundation of math.

- Use Hoare logic to reason about programs, using your logic / foundation of math to deal with inferences that are not given by the rules of your Hoare logic, i.e. for Hoare's "Rule of Consequence".

There are several ways of connecting the two. One is Hoare type theory [1]. Another is using Characteristic Formulae [2, 3].

[1] G. A. Delbianco, A. Nanevski, Hoare-Style Reasoning with (Algebraic) Continuations.

[2] L. Aceto, A. Ingolfsdottir, Characteristic Formulae: From Automata to Logic.

[3] A. Chargueraud, Formal Software Verification Through Characteristic Formulae.

Which of the many possible, highly contentious, and mututally incompatible notions of "social benefit" do you recommend Google adopt, and why?

I'm afraid that's not the case. Generics are very easy to implement under the following reasonable conditions:

1. you don't care about performance (you simply 'box' everything),

2. you don't care about executable size (you simply specialise every generic definition to their concrete use cases -- this is what C++ compilers do),

3. you don't do reflection on types in generic definitions.

As "cinnamonheart" mentions in a sibling post, ML's generics are straightforward, and remain, despite hailing from the 1970, even today a shining example of programming language design. Unfortunately, Scala had to violate all three points above to maintain compatibility with Java, and the JVM.

I'm asking because I'm considering developing an Erlang-like approach to message-passing concurrency for Rust.

Would you be able to venture a guess why they are not more popular? I agree that basing Rust's concurrency on an Erlang-like model would not have been a good idea, for reasons mentioned in this thread. Nevertheless the sheer convenience of Erlang-style concurrency would nevertheless be useful in quite a few scenarios where Rust is used.

Is there currently a reasonably mature Erlang-style threading library for Rust? Something that is to Rust what Akka is to Scala?

I like the quote "Scala is one of the few programming languages from academia that has had a significant impact on the world as well as on programming languages research"!

It has been argued that the raise of the Catholic Church to power had a similar reason: catholic priests don't have offspring (at least in theory) hence priests cannot form dynasties and the advantages (for trust and cooperation) of shared descent don't apply, thus priests and hence the Catholic church were less of a threat to existing nobility than other organisations that can form dynasties based on descent. (Note that the Catholic Church is the oldest still existing organisation, and was at some point in history arguably the most powerful organisation in the world.)

I have no opinion on the truth or otherwise of this theory, but find it fascinating.

Aha, of course, just like the Berlin Wall was an "Anti-Fascist Protection Barrier"!

https://en.wikipedia.org/wiki/Berlin_Wall

   "Union invaded Poland" 
   in public gets you killed

Why? What is taught in schools about this part of Soviet history?

Russia isn't even the Soviet Union, and the leader at the time was Georgian.

   Our algorithm ...

Unless I completely misunderstand what you write, the approach you describe is the standard way of setting up SMT-solvers by interaction between a SAT solver with a theory solver. I think it is called lazy SMT or DPLL(T) in [1] where this approach seems to have been described first. [2] is also an interesting description of the phenomenon.

[1] H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, C. Tinelli, DPLL(T): Fast Decision Procedures. https://www.cs.upc.edu/~oliveras/espai/papers/dpllt.pdf

[1] R. Nieuwenhuis, A. Oliveras, C. Tinelli, Abstract DPLL and Abstract DPLL Modulo Theories. http://www.cs.upc.edu/~roberto/papers/lpar04.pdf