aeneasmackenzie

YNAB does support multi account split transactions, it’s just a combination of the split and transfer types. It’s not meant to support full accounting but it certainly supports that.

Typical proofs don’t cover side channels, just ISA semantics. With the big asterisk that most programs are running on top of an unverified kernel on an unverified machine-level blob on an unverified ISA implemented by an unverified chip, you can absolutely prove the behavior of programs. Lamport has an unusual attitude towards verification and comes towards it from a slightly different angle, and model checking is not a good approach to machine-level proofs.

Statutes as harsh as this have been tried but were repealed for unspecified reasons (Draco’s laws in Athens) or because juries wouldn’t convict in death penalty cases very often (England’s Bloody Code).

Will Sam “Bank Fraud Man” be punished for fraud? Could go either way. Adam “New Man” got away clean.

Lots of people, if they weren’t banned from F1 for being too good. The drivers are just shifting gears to keep the audience from getting bored since 1994.

The year is 3000AD. A 1 million cubic kilometer xenon detector cooled to 2K orbiting Neptune has not detected any WIMPs. Not to worry, the next one will be ten times bigger and at 0.5K.

There is a relativistic MOND theory that has predicted the CMB spectrum[0]. And perhaps. MOND is first of all observational. AeST is just the latest (and AFAIK best) attempt to create a theory that reproduces the MOND acceleration artifact.

0: https://tritonstation.com/2023/01/13/what-we-have-here-is-a-...

It’s not proof, but if it wasn’t even diamagnetic it would be over. It couldn't just be a magnet, it is repelled from both ends of a normal magnet, according to Chinese lab videos you can find in the thread.

You may be able to (entirely legally) part out the sets on bricklink, buy the generic bricks from webrick, and buy the specific bricks from bricklink sellers. This will be substantially cheaper and it’s an onboard into non-Lego building bricks which have gotten really good in the last few years. The glut of vendors selling copied Lego sets has given the field a bad name, but the brick design is out of patent and there are many sellers designing their own sets as well as selling MOCs.

I’m sorry, it never occurred to me that you’d think I was questioning the beating part. I was entirely addressing the teaching. If they were teaching you heresy, they were outside the Catholic Church by definition.

> The collapse of the Soviet Union, which Fisher believes represented the only real example of a working non-capitalist system

If it was working, why did it collapse?

There are lots of alternatives to capitalism but most of them are measured in mountains of skulls. No one has any difficulty imagining more, most people just noticed.

> The holy trinity wasn't known to Jesus at the time of his life or death. …

If this was beaten into you the school you went to was not Catholic or even Chalcedonian, which is a low, low bar. This appears to be some form of the heresy of kenoticism and your parents deserve a refund.

There was an idea going around a few years ago to split the keyboard in half then make each half a mouse. King’s Assembly as a (successful but fizzled) kickstarter about this but there were others. I thought it was a great idea but it seems no one makes them now.

The only relevant part of the article is the quote from the Council of Chalcedon:

> Following the holy Fathers, we unanimously teach and confess one and the same Son, our Lord Jesus Christ: the same perfect in divinity and perfect in humanity, the same truly God and truly man, composed of rational soul and body; consubstantial with the Father as to his divinity and consubstantial with us as to his humanity; "like us in all things but sin". He was begotten from the Father before all ages as to his divinity and in these last days, for us and for our salvation, was born as to his humanity of the virgin Mary, the Mother of God.

This is one such stark delineation. All Catholics are required to be inside it.

Jesus and the Father are equated in the very first verse of John.

I often wonder what could have been if cyclone got more adoption. I don't really think "rewrite it in cyclone" would be any more successful than "rewrite it in rust" but "incrementally port it to cyclone" could have been faster.

Unity asset files killed my attempt at a comprehensive binary encoding format spec language. There’s a header containing a list of block pointers. The blocks are compressed and the (several) files are sequential. Typically the first file is a resource containing a block of metadata describing object type formats, then object references keyed to the specified formats. The objects can have transparent references (PPtrs) to other objects in the resource file, or other files in the asset, or other files or objects in in other asset files. One asset file usually contains the master list of what object is in what file.

None of this is a true blocker, but your format has to contain sigma types and at that point you’re just writing a parser normally.

Usually these tools just bail out. This is fine for the domain. Any division where the divisor is not known nonzero is a bug even if it will never happen because you probably aren't sure it will never happen either.

> In contrast, thanks to its modularity and domain-awareness, Astrée can be made exceptionally precise, often to the point of pro­ducing exactly zero false alarms.

I will guess that when analyzing avionics code with no memory allocation it is perfect, and when analyzing other code it is merely great. I wonder what the recruiting pipeline from INRIA into AbsInt is like.

You can file seek in any language, but not in most file format DSLs (or this one, because it's local). The author mentions QuickBMS and thus is aware of this, but most academic format languages don't support it.

I like these data description languages but most of them just have support for sequential structures and don't support offsets within the file. These are very common in file formats created for use with C or a similar language, which is most of them. It's not hard to add but it destroys the elegance of the formalism.

If I used a matchmaking service and it provided me with "end your subscription to a dating service 90% of the time" matches I would be telling everyone I knew.

Conservatives don't like David Brooks either.

If you actually have the ability to make great matches, matches so good you are concerned you will lose two customers, you should be running a matchmaking service and not a dating website.

"dark matter but not as much" is still an improvement if you replace it with something better. If MOND predicted these observations and LCDM didn't it's reasonable to say that it is better.

I bought one of the parts on amazon and got a version that had either desynced audio or subtitles. It seemed like a speed mismatch as it got worse as the movie went on. I don't speak Tamil, but I can still tell who should be speaking and it became very hard to follow. There was no way to adjust the sync or track speed like in mpv.

Message received, I won't buy again.

I have listened to a fair amount of fan fiction read aloud with what seems to be the default Siri voice in the fanfiction.net app. Like watching something with subtitles, you don't hear the drone after a while. It does put a lot more emphasis on the quality of the writing, which can be rough with fanfic.

Why do you believe this problem is inevitable?

> VIII

What did you like about it? I honestly can’t think of anything that landed.

Plenty of people consider proof by contradiction a fast one, like all intuitionist mathematicians.