GregarianChild

8 ms·

1.
by GregarianChild 7mo ago
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
2.
by GregarianChild 7mo ago
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/bl
3.
by GregarianChild 8mo ago
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.
4.
by GregarianChild 8mo ago
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
5.
by GregarianChild 8mo ago
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 :=
6.
by GregarianChild 8mo ago
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
7.
by GregarianChild 8mo ago
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
8.
by GregarianChild 8mo ago
Since the point of program extraction from a prover is correctness, I wonder what kind of assertions you prove for STM in Rocq.
9.
by GregarianChild 8mo ago
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"?
10.
by GregarianChild 8mo ago
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 simpl
11.
by GregarianChild 1y ago
> 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
12.
by GregarianChild 1y ago
> 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&
13.
by GregarianChild 1y ago
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' architectu
14.
by GregarianChild 1y ago
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
15.
by GregarianChild 1y ago
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 compu
16.
by GregarianChild 1y ago
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...
17.
by GregarianChild 1y ago
This paper https://arxiv.org/abs/2407.02944 ventures some guesses how Nvidia does this, and runs experiments to confirm them.
18.
by GregarianChild 1y ago
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
19.
by GregarianChild 1y ago
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?
20.
by GregarianChild 1y ago
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 Ch
21.
by GregarianChild 1y ago
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 theories is to minimise impredicative cons
22.
by GregarianChild 1y ago
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 access, and • the lack of sufficient parallelis
23.
by GregarianChild 1y ago
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 to [1], the 128 bits in a word are used as follows: •
24.
by GregarianChild 1y ago
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 conjecture the latter. Maybe someone from Sandia is on
25.
by GregarianChild 2y ago
> 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 executing in parallel.
26.
by GregarianChild 2y ago
I agree that the RISC-V ecosystem has some issues that I hope will be sorted out. But not all RISC-V cores are "baby cores". I imagine that XiangShan [1], albeit student work, will spur work towards bigger, more performant OOO co
27.
by GregarianChild 2y ago
I'm very interested in the "Typed Program Analysis Without Encodings" paper. But I can't seem to find it online. Where do you suggest I look for it?
28.
by GregarianChild 2y ago
The 5th edition is seriously out of date. The last 15 years or so have seen massive changes in computer architecture, in particular the explosion of all manner of hardware accelerators, including modern GPUs. The 7th edition is supposed to
29.
by GregarianChild 2y ago
> if FP is "better" The term FP has lost precise meaning over time, and split into several related meanings. • Focus on the absence of side-effects. (E.g. Agda, but not Scala, Ocaml, F#) • Focus on the higher-order functions
30.
by GregarianChild 2y ago
For what it's worth, Scala is a multi-paradigm language and can be used as a pure OO language. This is a great way to start for programmers with an OO background

More ›