Viewing profile — GregarianChild

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 …

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:/…

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 …

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 s…

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 …

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…

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 be…

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

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 "concurren…

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)) fo…

> 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 …

> 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…

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 'neur…

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 …

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 f…

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-op…

This paper https://arxiv.org/abs/2407.02944 ventures some guesses how Nvidia does this, and runs experiments to confirm them.

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…

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?

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…

The "intersection of all sets such that" is not vague at all. It's perfectly formally defined in ZF* set theories. But it's impredicative. One of the guiding ideas behind type theo…

The reason that VLIW/EPIC architectures have not been successful that for mainstream workloads is the combination of • the "memory wall", • the static unpredictability of memory ac…

Modern GPU instructions are often VLIW and the compiler has to do a lot to schedule them. For example, Nvidia's Volta (from 2017) uses 128-bit to encode each instruction. According…

I'd be interested to learn who paid for this machine! Did Sandia pay list price? Or did SpiNNcloud Systems give it to Sandia for free (or at least for a heavily subsidsed price)? I…

> both parallelism and pipelining You are right, but this can be make more precise: pipelining is a specific form of parallelism. After all the different stages of the pipeline are…