zozbot234

507 ms·

3361.
by zozbot234 2y ago
It's precisely when "you have frequently, even in the same expression, dozens of different kinds of additions, multiplications, divisions, etc., between scalars, vectors, matrices, tensors, complex numbers, various kinds of physic
3362.
by zozbot234 2y ago
It looks like AMD's CDNA gpu's are supported by Mesa, which ought to suffice for Vulkan Compute and SYCL support. So there should be ways to run ML workloads on the hardware without going through HIP/ROCm.
3363.
by zozbot234 2y ago
You can use floats to accelerate interval arithmetic (which is "exact" in the sense of constructive real numbers) but that requires setting the correct rounding modes, and being aware of quirks in existing hardware floating point
3364.
by zozbot234 2y ago
Proof automation definitely counts as AI. Not all AI is based on machine learning or statistical methods, GOFAI is a thing too.
3365.
by zozbot234 2y ago
You can do a lot better than that. You can treat memory ranges coming from separate allocations as distinct segments, and pointers as tuples of a segment ID and a linear offset within the segment. This is essentially what systems like CHER
3366.
by zozbot234 2y ago
Arguably, generating verified C from a low-level focused subset of F* (Low*, used in the HACL project) is close enough to count as a "similar tool".
3367.
by zozbot234 2y ago
> If so, where is the code that generates Rust, I do not see any links to any source repos. The paper states that these developments will be released under open source licenses after the review process is completed, i.e. most likely, aft
3368.
by zozbot234 2y ago
Early versions of Rust "started out" with GC: the language was broadly similar to Golang, though with a lot of influence from Ocaml and functional languages more broadly. The comprehensive use of borrowck to avoid GC altogether
3369.
by zozbot234 2y ago
Tl;dr: cache is the new RAM; RAM is the new disk; disk is the new tape.
3370.
by zozbot234 2y ago
The book is being worked on here https://fr.wikisource.org/wiki/Livre:Saint-Simon_-_M%C3%A9mo... already (volume 1 of 20). Not the same edition as what OP is working with, but it's a start.
3371.
by zozbot234 2y ago
This article argues at considerable length that an "educational" language targeting complete novices should choose a keyword-heavy syntax like Wirth's Modula 2 as opposed to a terser one like C, prior to discussing more esote
3372.
by zozbot234 2y ago
> Is a $8000 MBP regular consumer hardware? If you don't think so, then the answer is probably no. The very first Apple McIntosh was not far from that price at its release. Adjusted for inflation of course.
3373.
by zozbot234 2y ago
> there is generally no formal geometric way to verify their correctness. There are formal models of synthetic (i.e. axiom-and-proof based) Euclidean geometry where proofs can in fact be verified. This is accomplished by rigorously de
3374.
by zozbot234 2y ago
AIUI the jury is still out as to whether wider decoders are feasible with RISC-V's 16-bit and 32-bit split. It's specifically designed to ensure that insn lengths and positions can be decoded as easily as possible, without introd
3375.
by zozbot234 2y ago
> provide a side project where all the extra bits that maybe people liked can grow a replacement The whole point of freedesktop.org was to provide such a side project in the first place. The fact that it doesn't seem to be doing th
3376.
by zozbot234 2y ago
There is some geometric equivalent for any formula that can be built using some arbitrary combination of the four operations of arithmetic, plus square roots. If you allow for either 3D geometry or origami folds, you can extend this allowi
3377.
by zozbot234 2y ago
It's not really "AI hardware", it's just HPC on a slightly smaller scale than the traditional sort. And it's still going to be useful for plenty of workloads regardless of the current AI frenzy.
3378.
by zozbot234 2y ago
> their main issue was that if kids cell phones were in their lockers, how would they text their parents to say they were ok when their school had a shooting. If the main purpose is just texting with their parents in case of emergency, t
3379.
by zozbot234 2y ago
A model that's trained on legal decisions can still be used to explore these questions, though. The model may end up being uncertain about which way the case will go, or even more strikingly, it may be confident about the outcome of
3380.
by zozbot234 2y ago
Intuitionistic logic also allows for negative statements, which then are entirely non-constructive. From a proofs-as-programs POV, this is just the observation that a proof is not just a program, but rather a program plus an explanation of
3381.
by zozbot234 2y ago
Yup, there's also a huge amount of copyright-free, public domain content on the Internet which just has to be transcribed, and would provide plenty of valuable training to a LLM on all sorts of varied language use. (Then you could use
3382.
by zozbot234 2y ago
Synthetic datasets are useless (other than for very specific purposes, such as enforcing known strong priors, and even then it's way better to do it directly by changing the architecture). You're better off spending that compute
3383.
by zozbot234 2y ago
I assume that you're familiar with Maxima? It's perhaps the most commonly used open-source CAS - there are some emerging alternatives like Sympy. That aside, yes it's interesting that an old program from 1998 can still serve
3384.
by zozbot234 2y ago
> Constructionism is based on the fact that every proof is a construction, which corresponds to a program I don't think this is correct, even in constructive logic. Negative statements do not correspond to a construction, and in fa
3385.
by zozbot234 2y ago
Agda 1 (more specifically, the included UI program known as Alfa) implemented an automated translation from formal proof to natural language, driven via Grammatical Framework. This requires writing snippets of code to translate every singl
3386.
by zozbot234 2y ago
A C++ reference is more like a Rust &UnsafeCell<T> in practice - and there are thorny issues around the possibility of null references in C++ (which are supposed to be insta-UB per the C++ standard but are allowed by most compiler
3387.
by zozbot234 2y ago
> "supposedly" Rust's architecture support for all but the most popular archs is horrendous. Unpopular architectures are a bit of a pain. But what if you compiled from Rust to WASM and then transpiled the WASM object code
3388.
by zozbot234 2y ago
I think it's just not feasible to totally avoid the GC in a language such as Haskell. It's inherently involved in anything that would require heap-allocated data in C/C++, and more besides. For example, Haskell does not hav
3389.
by zozbot234 2y ago
> it is best if they are written in a language which makes the developers more productive than Rust does. AIUI, recent assessments (including by Google) have found that Rust developers' productivity is competitive with GC languages
3390.
by zozbot234 2y ago
I think most async runtimes give you the option of launching a single-threaded executor when you explicitly request it. AIUI the most esoteric tradeoffs wrt. GC involve how to have data representations that can be efficiently traced, and wh

More ›