GregarianChild

5 months agodiscuss

The question: "does the ambient programming language do the right thing?" applies to other provers too. So if you assume the semantics of the implementation language is broken, or the compiler, or the computer executing the code, then those issues also need to be added to the TBC of Curry-Howard provers.

There is no free lunch.

GregarianChild

5 months agodiscuss

This is wrong as the others replies also point out. Tactics in LCF-style provers are not part of the TCB. Here is an example of the TCB for an industrial strength prover:

○ https://github.com/jrh13/hol-light/blob/master/fusion.ml

A mere 676 LoCs. This miniscule size of the TCB is where the comparatively lesser bug count (despite intense use) comes from.

GregarianChild

5 months agodiscuss

LCF-style provers like Isabelle/HOL and HOLlight are some of the most widely used, and oldest interactive theorem provers. If they consistently show smaller error rates than other systems, that is an interesting empirical observation. To give but one recent example: Amazon recently announced a vast 260000 lines of Isabelle/HOL-checked correctness proof of their new Nitro hypervisor for AWS EC2 Graviton5 instances.

LCF-style provers have a much smaller trusted computing base than Curry/Howard based provers like Coq, Agda and Lean.

One may wonder if there is a correlation between size of TCB and error rate in widely used provers?

GregarianChild

5 months agodiscuss

There are some issues arising from size inconsistencies (AKA Cantor's Paradox) if / when you try to fit the representation of all internal choices (this could be infinite) into a small universe of a theorem prover's inductive types. The ChoiceTree paper solves this with a specific encoding. I'm currently wondering how to port this trick from COq/Rocq to Lean4.

GregarianChild

6 months agodiscuss

I'm not an expert in this field, but the way I understand it is that Choice Trees extend the ITree signature by adding a choice operator. Some variant of this:

ITrees:

    CoInductive itree (E : Type -> Type) (R : Type) : Type :=
    | Ret (r : R)                                                                                                                                                                                                         
    | Tau (t : itree E R)                                                                                                                                                                                                 
    | Vis {T : Type} (e : E T) (k : T -> itree E R)

ChoiceTrees:

    CoInductive ctree (E : Type -> Type) (C : Type -> Type) (R : Type) : Type :=
    | Ret (r : R)                                                                                                                                                                                                         
    | Tau (t : ctree E C R)                                                                                                                                                                                               
    | Vis {T : Type} (e : E T) (k : T -> ctree E C R)                                                                                                                                                                     
    | Choice {T : Type} (c : C T) (k : T -> ctree E C R)

One can see "Choice" constructor as modelling internal non-determinism, complementing the external non-determinism that ITrees already allow with "Vis" and that arises from interaction with the environment. (Process calculi like CCS, CSP and Pi, as well as session types and linear logic also make this distinction).

GregarianChild

6 months agodiscuss

Thanks. I hope you publish this.

I imagine https://github.com/bloomberg/crane/blob/main/theories/Monads... is the functional specification of STM. I see that you use ITrees. WHat's the reason for not using Choice Trees that tend to be easier for handling non-determinism?

GregarianChild

6 months agodiscuss

This definition is my potentially flawed attempt at summarising the essence of what program extraction is intended to do (however imperfect in practise).

I think extraction goes beyond 'mere' compilation. Otherwise we did not need to program inside an ITP. I do agree that the state-of-the-art does not really full reach this platonic ideal

GregarianChild

6 months agodiscuss

Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.

GregarianChild

6 months agodiscuss

I have another question, the abstract of your paper says that you "provide concurrency primitives in Rocq". But this is not really explained in the text. What are those "concurrency primitives"?

GregarianChild

6 months agodiscuss

I would phrase it a little different.

Simplifying a bit, a compiler tr(.) translates from a source language L1 to a target language L2 such that

    semantics(P) == semantics(tr(P))

for all programs in L1. In contrast, and again simplifying a bit, extraction extr(.) assumes not only language L1 and L2 as above, but, at least conceptually, also corresponding specification languages S1 and S2 (aka logics). Whenever P |= phi and extr(P, phi) = (P', phi') then not just

    semantics(P) == semantics(P')

as in compilation, but also

    semantics(phi) = semantics(phi'),

hence P' |= phi'.

I say "at least conceptually" above, because this specificatyion is often not lowered into a different logical formalism. Instead it is implied / assumed that if the extraction mechanism was correct, then the specification could also be lowered ...

GregarianChild

10 months agodiscuss

> fantasy of yours that never happened

Shall we bet money on this?

You are right, I don't know much about SpiNNaker. All I know about SpiNNaker is from a talk of Furber's where he said "Neuromorphic status: attracts no money, but works (in the sense of accelerate in niche domains)". When I asked niche domains, he replied: "brain simulation but nothing else".

> understood nothing about dataflow as a way to reduce energy consumption (as your last post proved).

If you don't tell me concretely, where I am wrong about dataflow, I cannot learn and improve ...

GregarianChild

10 months agodiscuss

> definition of the word neuromorphic

The definition of the term is so vague as to be useless for scientific progress. What exactly is excluded by "brain inspired"? If I paint my computer grey because the brain is grey, it's brain inspired? You know that regular expressions were invented to model neurons [1]? If nothing is excluded the term is useless. But in reality, the term is used explicitly to deceive as already done in the 19th century see [2].

Heraclitus says somewhere something to the effect that "good thinking is dry". Established terminology like

• Asynchronous CPU

• Delay Insensitive Circuit

• Quasi-Delay-Insensitive Circuit

• Clockless CPU

• Asynchronous circuit

• Self-timed circuit

is dry and useful. 'Neuromorphic' suggests an understanding of how the brain works that is just not there in 2025.

> Do we know that neurons operate asynchronously to each other, only activating when their inputs change? Yes.

I strongly disagree.

We do not know how exactly the brain codes information. If you have timed coding, it's not asynchronous. And that doesn't even address the chemical signals that abound in the brain. The Hodgkin-Huxley equations give a good approximation to how the neuron produces a "spike" - the signal that travels down the axon. But it's only an approximation. Every type of ion channel in the cell adds another 10 or so unkown parameters to the equations, which can only be approximately found experimentally. So we have a fairly good picture of how a single neuron behaves in most circumstances, but not complete. Ion channels are are crucial to how the brain works. They are the nonlinearity that makes computation possible, like the transistor is to the computer. There are several hundred types of ion channel that are known about so far and probably thousands more that are not yet discovered.

> That's a silly question

Not in the context I asked: I asked him after he had suggested that 'neuromorphic' would be great to reduce the energy consumption of LLMs. I wanted to know why/how, given that LLMs are trained today with BP. I give him the benefit of the doubt here, since we were in a rush and could not go deeper into the subject.

> mix spiking neural nets and backprop ?!

It's an active area of research to do just this. Google SpikeProp, e.g. [3]. Lot's of papers in this space at the moment. Why? I don't know as I don't follow this space. Potential reasons: (i) BP is natural, (ii) BP works super well for DeepLearning, (iii) the 'neuromorphic' community has failed so spectacular and want to try something that works, (iv) to get funding, (v) we really do not know how the brain works, and in that case, why not try out crazy things?

[1] S. Kleene, Representation of events in nerve nets and finite automata. https://www.dlsi.ua.es/~mlf/nnafmc/papers/kleene56representa....

[2] K. S. Kendler, A history of metaphorical brain talk in psychiatry. https://www.nature.com/articles/s41380-025-03053-6

[3] https://homepages.cwi.nl/~sbohte/publication/esann.pdf

GregarianChild

10 months agodiscuss

I don't rate Furber as a "complete amateur", but he's the exception in this milieu.

> Neuromorphic just means brain-like or brain inspired,

I don't even see any evidence that 'neuromorphic' architecture is brain inspired in a non-trivial sense. Can you please provide evidence, for example, a non-trivial mapping between 'neuromorphic' architectures (say SpiNNaker) and the SOTA models of the brain that we have, e.g. the existing data-driven model simulating C. elegans brain (the MetaWorm project)?

As Steve Furber also says (personal communication): we don't know enough of how the brain works to have computer architectures that can meaningfully inspired by brains. The "neuro-" prefix is marketing. [1] documents this use and dates it back to the 19th century. See also

• Neuroergonomics

• Neurotypical

• Neurodivergent

• Neurodiverse

• Neurosis

• Neuroethics

• Neuroeconomics

• Neuromarketing

• Neurolaw

• Neurosecurity

• Neuropsychology

• Neuropsychoanalysis

• Neurotheology

• Neuro-Linguistic Programming

• Neurogastronomy

I have seen all the above used without irony.

> brains operate in asynchronous dataflow type fashion.

That's a questionable statement. To the best of my knowledge, there is no consensus as of 2025 of how to model even a single neuron. (Function of synapse is even less understood).

When I asked Steve Furber what 'neuromorphic meant, he said: "There are many things today described as neuromphric. Mead would not call SpiNNaker as neuromorphic!"

Furber also said: "Neuromorphic status: attracts no money, but works (in the sense of accelerate in niche domains)". Upon my asking what niche domains, he said: "brain simulation but nothing else". (He was referring to SpiNNacker). I asked him if SpiNNaker can accelerate back-propagation and he said: "no, because the brain does not do back-propagation".

> async (dataflow) processor design, while complex, clearly isn't an impossible task

I did not say it was impossible. It has been done many times, see my references to Arvind's lab at MIT (I spent some time there). The problem with async (dataflow) processor design is that it consistently fails to live up to its promises (PPA). There are specific technical reason for that that are quite well understood.

> why you focus on "general purpose processors" given that we're talking about ANNs and neuromorphic systems.

Because the 'neuromorphic' marketing often reads like they want to build more efficient 'brain-inspired' general purpose computers. Certainly the dataflow architectures (a la Arvind/MIT) tried to. This is one of the many issues with the 'neuromorphic' milieu: they are really vague about their goals. If they would restrict their claims to certain classes of accelerators, then their claims would be less delusional.

> the goal is to minimize power usage.

If that is the goal, they are also not very successful. On CMOS silicon changes from 0 to 1 or 0 to 1 is what consumes most of the power, this would make the constant spiking expensive, no?

[1] K. S. Kendler, A history of metaphorical brain talk in psychiatry. https://www.nature.com/articles/s41380-025-03053-6

GregarianChild

10 months agodiscuss

Can you explain the benefit of renaming dataflow as 'neuromorphic'?

You do understand that dataflow architectures have been tried many many times? See [1] for a brief history. MIT had a bit dataflow lab for many years (lead by the recently deceased Arvind). What is the benefit of re-inventing dataflow architectures by complete amateurs who are not at all aware of the 1/2 century research tradition on dataflow architecture, and the very clear and concrete reasons when this architecture has so far failed whenever it was tried for general purpose processors?

We can not even apply Santayana's "those who forget their history are condemned to repeat it because the 'neuromorphic' milieu doesn't even bother understanding this history.

[1] https://csg.csail.mit.edu/Dataflow/talks/DennisTalk.pdf

GregarianChild

10 months agodiscuss

The 'brain-inspired' community has always been doing this, since Carver Mead introduced the term 'neuromorphic' in the late 1980s. Reselling banalities as a new great insight. My favourite is "Neuromorphic computing breakthrough could enable blockchain on Mars" [1]. What else can they do? After all, that community has now multiple decades of failure under it's belt. Not a single success. Failure to make progress in AI and failure to say anything of interest about the brain. To paraphrase a US president: In this world nothing can be said to be certain, except death, taxes and neuromphicists exaggerating. (Aside: I was told by someone who applied to YC with a 'neuromorphic' startup that YC said, they don't fund 'neuromorphic'. I am not sure about details ...). The whole 'brain talk' malarkey goes back way longer. In particular psychology and related subjects, since their origins as a specialty in the 19th century, have heavily used brain-inspired metaphors that were intended to mislead. Already in the 19th century that was criticised. See [3] for an interesting discussion.

There is something interesting in this post, namely that it's based on non-Nvidia GPUs, in this case MetaX [2]. I don't know how competitive MetaX are today, but I would not bet against China in the longer term.

[1] https://cointelegraph.com/news/neuromorphic-computing-breakt...

[2] https://en.wikipedia.org/wiki/MetaX

[3] K. S. Kendler, A history of metaphorical brain talk in psychiatry. https://www.nature.com/articles/s41380-025-03053-6

comments