xavxav

7 ms·

31.
by xavxav 3y ago
I'm not familiar with the structure of stream payouts on Spotify, but if 80 million streams gives 12 dollars, that means Taylor Swift's 26.1B streams give ~4k? I knew the rates were bad but damn...
32.
by xavxav 3y ago
A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust. The trust in a Coq proof comes down to "do you believe that the 8kloc kernel fa
33.
by xavxav 3y ago
> Can someone familiar explain why it's difficult, say, in an imperative language, to represent mathematical notation? Is the question whether you can represent mathematical notation in an imperative language, or whether you can sea
34.
by xavxav 3y ago
wow that's really cool, I wonder what the essential difference is between type-in-type and other classic "nice" inconsistencies in type theories. It seems like it's "almost" consistent.
35.
by xavxav 3y ago
I'm tired and cranky today so this will lack subtlety, but: You don't have to use Rust but you **can't** use C. There's no reason to be finding these bugs in 2023; period, we can do better and we know how to
36.
by xavxav 3y ago
Yes, but I you cut and store the wood at maturity you could plant fresh trees instead. The point is, trees are an entirely inadequate solution to climate change, at least on the CO2 front.
37.
by xavxav 3y ago
It takes ~40 trees to capture one ton per year, with ~40B tons emitted each year, that means planting roughly 160B trees each year . Humans have changed the world in a manner which natural ecosystems cannot recover on their own. We need to
38.
by xavxav 3y ago
A project I've always toyed with in my head is a fancier version that would count / verify the checks have all entered the coop at closing time and warn you if not. With my parents coop occasionally a chicken will decide to brave
39.
by xavxav 3y ago
> It sounds like a profound wisdom and on a very surface level it does make sense, but think of this: if you can assess that a measure is a bad one, this means that you have your own intrinsic preferences, otherwise you wouldn't be
40.
by xavxav 3y ago
Compiling to C is definitely an option, but there are also plenty of low-hanging fruit that could come before. You could invest in a better interpreter or even some bytecode compilation first. I don't know where your rules are coming f
41.
by xavxav 3y ago
I really want a good health tracker with all the sensors of the Apple Watch but completely inconspicuous as smartwatches are ugly.
42.
by xavxav 3y ago
Unrelated, but your homepage has very bad FPS using firefox on mac due to the animation. Once I manage to scroll it works quite well.
43.
by xavxav 3y ago
They aren’t unless you’re willing to go significantly more complex than this naive translation suggests. As an example, consider the index_mut function with signature fn index_mut(&mut Vec<T>, ix: usize) -> &mut T H
44.
by xavxav 3y ago
> The borrow checker in Rust might be to important to turn off even sometimes. Variations of this point come up often, that the main reason rust compile time is slow is typechecking or borrowchecking, but that’s not true, while those ope
45.
by xavxav 3y ago
Oh right this is just Horn clauses, not CHCs
46.
by xavxav 3y ago
Z3 is actually not a particularly good SAT solver, you really want to use a dedicated tool for pure SAT problems. On the other hand if your problem is in a richer class like QBF or SMT then z3 shines and often you can use encoding tricks to
47.
by xavxav 3y ago
Wait, this is very relevant to some work I’ve been doing recently, how do you conclude that Horn clauses should be preferred from Schaefer’s theorem?
48.
by xavxav 3y ago
Indeed, but CreuSAT is actually a high-performance implementation (ie: worst of the best), I should probably just write up a Rust gist of CDCL.
49.
by xavxav 3y ago
Conflict explanation in CDCL is entirely based around resolution, the idea being to take a conflicting set of clauses and apply resolution a bunch of times to “simplify” the conflict into its most general form.
50.
by xavxav 3y ago
I almost exclusively use it with quantifiers which makes it equivalent to FOL. But even without quantifiers, theory combinations can introduce undecidability. There’s the auxiliary problem that decidable but slow can often be equivalent to
51.
by xavxav 3y ago
A fun exercise is to write a series of sat solvers: brute force, DPLL and CDCL you really get an immediate feel for the strength of the algorithms and none of these implementations need to go much beyond 50-100 lines in a modern language.
52.
by xavxav 3y ago
I wonder if they'll write a followup on the SMT revolution that happened after the CDCL breakthroughs for SAT. The lazy approach to SMT was a huge step forward, but itself spawned a whole lineage of refinements, alternatives and change
53.
by xavxav 3y ago
On its face I'm not against using analogies to explain scale, but its not like i really have an intuitive grasp on the size of a 747 or a football field's volume. It also helps to remember that 1m^3 is 1000L which allows you to tr
54.
by xavxav 3y ago
I have a commented example: https://github.com/xldenis/besm/blob/master/examples/chapter... I tried to transliterate the syntax to ascii but the 'real' syntax uses some characters which ar
55.
by xavxav 3y ago
Indeed, I only provided direct translations of the programs Ershov and Knuth wrote, I never did much in the way work beyond that, my focus was mainly on recreating the compiler itself. For that I actually copied the pages of the book into t
56.
by xavxav 3y ago
I have perused those archives many times, more important than the book (of which I have a translated hardback copy), are the notes which include the hand written (and commented) assembly for every draft of the compiler. The hard part is tha
57.
by xavxav 3y ago
Hi! I'm the author of this project :) Happy to answer any questions, and yes I know I need to finish it. The project includes a VM for the BESM which I think has pretty sexy visuals: https://twitter.com/xldenis/sta
58.
by xavxav 3y ago
Oh I love this project, its very interesting to think about its relation to the family tree of soviet programming languages. From the start (ie: 1946-48) they conceptualized programming through the notional of 'logical schemas' or
59.
by xavxav 3y ago
I couldn't tell if this was satire or not but it seems to be completely serious?
60.
by xavxav 3y ago
On second thought, these are mostly too closely related, I think that if you want to truly find the ur-specification languages this is closely related to Girard's research program. Specification languages are intrinsically tied to a no

More ›