thaliaarchi

9 ms·

31.
by thaliaarchi 3y ago
Film can be physically re-scanned at a higher digital resolution—no AI required. The title says “4k Film Transfer”, which suggests this.
32.
by thaliaarchi 3y ago
A rendered Markdown version of this book is available here: https://xmonader.github.io/letsbuildacompiler-pretty/
33.
by thaliaarchi 3y ago
That's a lot of steps in your bootstrap chain. I think tying it to releases can make it easier, but it's good your process is automated. Rust has a long chain too, but rustc only uses features itself, that the previous release sup
34.
by thaliaarchi 3y ago
You should definitely publish that and comment a link! That would be very useful, since you got much further than me.
35.
by thaliaarchi 3y ago
I like that term. I've tried a couple of bootstrap pilgrimages. For a job, we needed Go on FreeBSD 8, which entailed a local patch to revert pipe2 to pipe in Go, and building from source. That was my first bootstrap. Go, as Russ mentio
36.
by thaliaarchi 3y ago
https://developer.mozilla.org/en-US/docs/Web/Text_fragments
37.
by thaliaarchi 3y ago
The malloc design, that led to that yacc bug being discovered, seems to have another interesting property which I didn't see discussed there: By placing large allocations (those larger than half the page size) at the end of a page, I w
38.
by thaliaarchi 3y ago
I'm surprised to see that the author's ipnsort is not published on crates.io, even though it performs at first or second place on most of the benchmarks for unstable sorts and it passes all the safety and correctness criteria, all
39.
by thaliaarchi 3y ago
I know of at least four MIRs. I used NIR as the name of the IR of one of my compilers. It's not a big deal. Just add qualifiers to your searches.
40.
by thaliaarchi 3y ago
For source code, I prefer the Software Heritage archive over the Internet Archive, because it archives the git history, instead of the HTML UI. This particular repo was saved there[0] and was most recently visited 24 Oct 2022, which has two
41.
by thaliaarchi 3y ago
Right, not all of the techniques shown yield code that’s correct by construction. For example, an argument was indirectly given, and that error was only found after writing a theorem involving it and finding it was impossible to prove. In t
42.
by thaliaarchi 3y ago
The only useful ltac I see in there is compare, which can save a lot of tedious rewrites, when needing that frequently.
43.
by thaliaarchi 3y ago
The post also links to some examples of using Wasm to solve complex typographical problems, which I found interesting. https://github.com/harfbuzz/harfbuzz-wasm-examples
44.
by thaliaarchi 3y ago
This reminds me of when I used zeroeth, oneth, twoth, and threeth, instead of first, second, and third, for referring to indices 0, 1, 2, and 3 as a TA. It's less verbose than “at index zero”, but feels a little clumsy.
45.
by thaliaarchi 3y ago
I’m surprised by the low counts for Patient Skeleton. I would have thought stale PRs would be merged more frequently.
46.
by thaliaarchi 3y ago
For anyone confused here, the “simple” here comes from the simply-typed lambda calculus, that it models. This post addresses several issues with a tutorial paper on a dependently-typed lambda calculus, which is what all the build-up is fo
47.
by thaliaarchi 3y ago
Additionally, LLVM has MIR (Machine IR), which is what Zig's also stands for. There's a lot of M-starting compiler intermediate representations. This Ruby MIR is Medium Internal Representation. Rust's is Mid-level IR. Similar
48.
by thaliaarchi 3y ago
MIR for Ruby is in no way related to Canonical Mir.
49.
by thaliaarchi 3y ago
The trick for preserving array lengths in function signatures looks quite useful (e.g., `void foo(int p[static 1]);` for a non-null pointer p). Unfortunately, I think the overloaded use of `const` and `static` somewhat obfuscates its seman
50.
by thaliaarchi 3y ago
Somewhat related to this, printf alone in a loop is Turing-complete, by using %-directives like that. It was introduced in “Control-Flow Bending: On the Effectiveness of Control-Flow Integrity” (Carlini, et al. 2015) and the authors have im
51.
by thaliaarchi 3y ago
Andrew Kelley even referenced this in the proposal: > In exchange, Zig gains these benefits: > - All our bugs are belong to us. > - …
52.
by thaliaarchi 3y ago
The commit that caused OP's bug changed two lines. https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/lin...
53.
by thaliaarchi 3y ago
You may also want to take a look at “Deletion: The curse of the red-black tree” (Germane and Might 2014), which presents functional deletion for red-black trees. https://matt.might.net/papers/germane2014deletion.pdf
54.
by thaliaarchi 3y ago
How does Datalog with e-graphs compare to Datalog with BDDs in terms of what analyses can be performed? bddbddb is a Datalog engine using BDDs, that, according to their 2005 paper[0], can solve problems like context-sensitive pointer analys
55.
by thaliaarchi 3y ago
Do you have a favorite dictionary for Fremdwörter?
56.
by thaliaarchi 3y ago
From Nand to Tetris: Building a Computer from First Principles https://www.nand2tetris.org/
57.
by thaliaarchi 3y ago
How does egglog compare to bddbddb, a Datalog engine powered by BDDs? They use BDDs in Datalog to solve previously unsolved problems like context-sensitive pointer analysis for large programs and show that analyses implemented with it are f
58.
by thaliaarchi 3y ago
This is the automatic resolution of some instance satisfying a typeclass constraint, and is not related to the termination of functions. This does not call a function. If you compare it to the relational definition I give at the end of the
59.
by thaliaarchi 3y ago
I was referring to how the communities of these languages typically frame the problem, so you need formal background to read the materials published on it. As you say, this is a major barrier. This is where Rust shines, in that they've
60.
by thaliaarchi 3y ago
I was not familiar with loader.c, so I did some digging[0]. It implements the Calculus of Constructions, which Coq is based upon, and generates all programs encoded lower than some value. The search is halting, though very long. From the an

More ›