GregarianChild

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

GregarianChild

hace 6 mesesdiscuss

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

hace 6 mesesdiscuss

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

hace 11 mesesdiscuss

> 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

hace 11 mesesdiscuss

> 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

hace 11 mesesdiscuss

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

hace 11 mesesdiscuss

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

hace 11 mesesdiscuss

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

GregarianChild

hace 11 mesesdiscuss

There is an old CACM post that explains how to use a bit of randomness to avoid only doing semantics preserving program changes.

https://cacm.acm.org/research/stochastic-program-optimizatio...

GregarianChild

hace 11 mesesdiscuss

This paper

https://arxiv.org/abs/2407.02944

ventures some guesses how Nvidia does this, and runs experiments to confirm them.

GregarianChild

hace 11 mesesdiscuss

If the search space never leaves the programs that are equivalent to the original specification, that will probably limit the optimisations you can discover. (E.g. if you start out with standard matmul, you will not discover Strassen's algorithm.) This is not a criticism, I'm just trying to understand your algorithm.

GregarianChild

hace 11 mesesdiscuss

How is this different from superoptimisation?

Also, how do you ensure that newly generated kernels are correct w.r.t. the original naive kernel that you use as specification?

GregarianChild

el año pasadodiscuss

Chisel has a compiler to Verilog. That is not the problem. Many semi-companies use a tool-chain to generate much Verilog from higher-level sources.

The rumour I heard was this: The problem with Chisel was that (at least in the past) the Chisel compiler did not preserve port structure well. So if you had a Chisel file that translated to 80M LoCs Verilog, then verified the 80M Verilog (which is very expensive), then made a tiny change to the source Chisel, the resulting new Verilog uses different port names even for the parts that were not affected by the change. (To quip: the (old?) Chisel compiler was a bit of a hash function ...) So you have to re-verify the whole 80M of Verilog. That is prohibitively expensive, compared to only reverifying the parts that truely need to change. The high verification costs forced by this problem were rumoured to nearly have sank a company.

This is a compiler problem, not a Chisel language problem. I was told that the compiler problem has been fixed since. But I did not check this.

GregarianChild

Submissions

Reevaluating Google's Reinforcement Learning for IC Macro Placement (AlphaChip)

Interview with Jim Keller: 'The Laziest Person at Tesla'

Intel Reportedly Offers over $2B to Acquire the Fabless Semiconductor SiFive

Hedge fund urges Intel to explore deal options

Estimating the Dollar Cost of LLVM

Estimating the Dollar Cost of LLVM

Wearing a Face Mask Is Encouraged in Asia, Shunned in the U.S.

comments