

So what formal language do you think would be more appropriate than Lean for this purpose?
Professional software engineer, musician, gamer, stoic, democratic socialist


So what formal language do you think would be more appropriate than Lean for this purpose?


Then what was your point?


not mathematically complicated but logically complicated
Lean is more than capable of modeling logic.


Forgive me if I’m off base, because I have not used jquery personally, but from what I’ve read, jQuery is both redundant and has a lot of footguns. I think it’s reasonable for people to discourage its use, especially for new applications that simply don’t need it.


You could use that to run the TisVlay CLI to automate TV related macros
Nice idea. I may try this out next time I’m tweaking my NixOS configs.
But for speaker bars/stereos, that’s another idea to add to the HDMI-CEC backend.
Yea that definitely sounds interesting. My speakers are connected over optical digital audio cables. I can’t even control them with my TV remote. I’m not sure I will be able to make this work. But I am planning on getting a new TV soon so 🤞


I use Plasma Bigscreen for my HTPC. I can’t speak to development status, but I know that it is functional for me as I use it daily. I use it for two things: moonlight game streaming client and jellyfin client. I can use the KDE Connect android app as a remote, but more often I use a bluetooth game controller or the Jellyfin android app to cast stuff.
It’s basically never locked because I don’t need it to be.
I don’t have an OLED TV yet, so the burn in prevention stuff isn’t useful to me yet. But having things like power and volume control on my phone would be really nice QoL improvements. I currently need to use my TV remote for power and input selection and my speaker remote for volume (though at least Jellyfin has its own volume control too).


Nice! Thanks for sharing!
I’m curious if you’ve used Plasma Bigscreen, what you think of it, and how TisVlay would integrate with it.


I think that’s kind of the point though. It really highlights the hypocrisy if a tech company that uses LLMs ever tried to sue claiming that using LLMs violates their copyright.


You could say the same about patents for physical inventions. But there are legitimate reasons for patents to exist.


It’s a term AI bros came up with to describe replacing the entire development lifecycle with AI.


Software factories
🤮


Be the change you want to see in the world. Find a physical copy, rip it, upload it.


There are private trackers where you can earn a currency based on seeding uptime, not actual upload. Then you can spend the currency to get more download buffer. Farm the currency by just downloading and seeding a bunch of freeleech stuff.


I know what you mean, but this is also essentially the same rhetoric that actual racists use to refute good policies like DEI. Diversity is a good thing, and I’m not sure you can achieve it by letting everyone self-police their behavior towards someone of a different race. Racism simply exists in our culture whether or not people are aware of it, so we need policies that counteract it.
Maybe a more persuasive way of saying the same thing: if you agree that some ethnicities or social demographics are historically disadvantaged and need more help than others, why would you not try to focus policy to prioritize their needs? It’s similar to making policy that reduces child suffering at the expense of some freedoms for adults.
That said, I also believe it’s good to try making policy that doesn’t explicitly target specific races if possible. For example, strengthening workers’ rights in general improves the lives of an entire economic class, and coincidentally it would disproportionately help Black and Mexican people (per capita).


I play a card game called Spitzer, where one of the rules is that the holders of the two black queens end up on a team. It is incredibly common to say things like “you beat the blacks”, etc. Context is everything.


While funny, the hero could have done both: save them and register them as organ donors.


Just because someone making such an argument identifies as a utilitarian doesn’t mean all utilitarians make flimsy arguments.


You are correct to point out the distinction between race conditions and data races. Rust only rules out data races.
I don’t know whether the race in question was a data race or not.
I would still wager that Rust code generally has fewer race conditions than C, given that mutable aliasing can be used as symbolic prevention of race conditions, i.e. your &mut T doesn’t necessarily need to hold data; it can represent some domain concept.
aren’t language specific
There are actually languages that guarantee deterministic concurrent execution, and this can rule out larger classes of race conditions than just data races. See the Bloom language and CALM theorem.




My god what an obnoxious website.