[ home / rules / faq ] [ overboard / sfw / alt ] [ leftypol / siberia / hobby / tech / edu / games / anime / music / draw / AKM ] [ meta / roulette ] [ cytube / git ] [ GET / ref / marx / booru / zine ]

/tech/ - Technology

"Technology reveals the active relation of man to nature" - Karl Marx
Password (For file deletion.)

Join our Matrix Chat <=> IRC: #leftypol on Rizon

| Catalog | Home

File: 1643229232223.jpg (55.47 KB, 1000x669, gno.jpg)


I told you about proprietary services man
I told you dog
9 posts omitted. Click reply to view.


Can anyone explain to me what formal verification is like I'm a complete idiot
I have a little programming experience and even commited to an open source project but can't wrap my head aroound that


I'm not an expert but I've talked to a sel4 engineer in person.

In mathematics, there are formal proofs.
We can make a mathematical statement and show that our stated assumptions guarantee the result is true.
(further interesting stuff) https://en.wikipedia.org/wiki/List_of_mathematical_proofs

We can also apply a similar concept to software algorithms. I haven't looked into the techniques myself so I can't explain them, but essentially you can provide a formal proof on an abstract mathematical model of the system. Provided that model is accurate, it formally verifies the program does the defined function, no exceptions. You have a guarantee that the code's implementation does what was specified. That's very good for important things like cryptographic code where correctness is important.

This doesn't mean it's 'unhackable' or infallable: what if the actual design specification has issues? Then they're provably in the implementation! But it does remove a lot of potential issues and bugs since there aren't any implementation bugs. Implementation bugs are a HUGE source of software security vulnerabilities.

Here's an example of a microkernel that has (partial) formal verification:
>A formal proof of functional correctness was completed in 2009. The proof provides a guarantee that the kernel's implementation is correct against its specification, and implies that it is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.
So that shows some of the kind of issues verification can avoid, which would potentially lead to a crash/failure or a security weakness if they were in there.


>neither musl nor glibc use formal verification, so there's no way to know if either is safe
binary-brain shit. there's no thing as 'safe/unsafe' to describe a whole program's security profile. and no, formal verification doesn't make it 100% safe, although it can have very great effects on improving it.

There are other things to consider:
>musl: closer fit to specification
>musl: decreased attack surface
>glibc: more eyes, more testers (and more attackers)


>binary-brain shit
normie detected
>describe a whole program's security profile
we're talking about libc, not an entire program. and yeah, of course it's contingent on the model you're using. duh
saying "musl has fewer CVEs" means nothing when much fewer systems use it and it hasn't been around for as long as >>13275 says
when you claim that A is more safe than B you must have something other than fee-fees to back that up. if you can't quantify said security then you are engaging in idealism


I hate compiling my own stuff and musl repos are lacking, or did they get better?

File: 1643960150530.mp4 (328.94 KB, 270x480, 2xpysu.mp4)


hey comrades have any of you ever encountered issues with the "antimalware services executable" process on Windows 11?
here's the run down:

>running windows 11

>8 gb RAM
>antimalware services executable runs ALL THE TIME
>eats up 50% of memory 24/7, absolute hell
>tried installing malwarebytes instead to disable it, problem just got worse
>turned off real time threat protection, processes still appear in task manager
>cant regedit bc tamper protection feature and i would like to avoid turning that off for security reasons
>already added exclusions for MsMpEng.exe, no change

and no, i cant just install linux, although i would like to. im fixing a laptop for someone else who can't afford to just upgrade and get more RAM.


File: 1643960936252.webm (216.39 KB, 1920x1080, windows-users.webm)


could be a bunch of corrupted files. try repairing or getting rid of them entirely with some tool


he could unironically upgrade by going back to windows 10 or seven tho,it's at least less intensive if you really want to keep windows.
can't you just remove the tamper protection in safe mode with no internet,and then put it back before restarting the computer ?
Also why would linux uses more RAM than this bullshit ?


He had the same issue on Windows 10, and he can't go back to 7.
The RAM comment was about how advice like "get more RAM" wouldn't work. I know Linux doesnt use as much RAM i'm not retarded. I can't switch the OS to any Linux distros because the user is disabled and has a perfect set up for his disability at the moment. It would be a lot of effort to get everything back to where it is and he doesn't have time.


i know this already, shut the fuck up unless you have any actual advice its not my god damn pooter

File: 1643987216277.png (360.9 KB, 512x512, Z7HeRxU.png)


More and more I feel I am being poisoned by the hyperonline shit I see every day. I am very much considering blocking my home router access to leftypol and 4chan, maybe even reddit. How do I do this? From what I've read https is not possible to routerban regularly, and the solutions I found require third party software that requires its own accounts etc. Is there any way to homebrew a lock which would deny my access to certain https sites on my router network?


how about just not visiting those sites

File: 1641718683789.png (1.09 MB, 1200x800, ClipboardImage.png)


Is stirring up again

Some article got written, the official @Android account is quoting it about bullying and what not

We can use this opportunity to point out how this is a class issue basically,
And how this silly joke has basically normalised classism against the poors who have android phones
17 posts and 2 image replies omitted. Click reply to view.


>Source: A trillion dollar company told me so


Literally only burgers and maybe their proxies care about this. Isn't Android the most widely used OS in the world? No on else cares.


lots of people across the world use iPhone. you're acting like it's a tiny share of the market and restricted to a single demographic


Apple is more used only in America and Japan lol


Being bullied because you don't have the same phone as the other kids is like the most burgerland dystopian thing ever.

File: 1632802148723.jpg (437.76 KB, 1281x720, giied.jpg)


Modern Hipster Codebases aren't using the GPL anymore ever since Microsoft started pushing the MIT as the default license for repos on github. M$ is doing its hardest to condemn us to proprietary software by encouraging the use of cuckold licenses. Imagine if the Greatest Computing Corporation somehow convinced all aspiring coders to start slapping together code that will be used in future microsoft projects… for free? That world already exists, for we live in a world where github is the most popular git site in the world.
78 posts and 6 image replies omitted. Click reply to view.


not that anon, but chromium can be a binary blob a lot of the time iirc, especially since the FOSS licensing is finicky to the point where a lot of it isn't exactly share-alike and people like the devs of electron can do whatever proprietary stuff they please


Electron is when basically when you write js and then ship it with chromium and node, end result of course being in hundreds of megabytes.
Freedom issues are basically same as those of chromium.
+ it just stinks as a technology

And chromium? Well, it might be technically free that is open source and under an fsf approved license iirc, but that doesn't matter, it still phones home and it's so complicated and huge it'll literally take longer to compile than the rest of your gnu linux distro combined, I think I needn't clarify its development can't be affected by anyone but google and its friends


>Take a look at your android phone
Google play services and the various spyware apps are proprietary, so no, it doens't count

>You can’t effectively build a walled garden with GPL code.
the very fact that you can install custom ROMs and root your android phone compared to the literal walled garden of iphone proves the point


>Google play services and the various spyware apps are proprietary, so no, it doens't count
I'm not talking about that even
>the very fact that you can install custom ROMs and root your android phone compared to the literal walled garden of iphone proves the point
Full of proprietary blobs + it's still android which means it's still user-mistreating misdesign built specifically to restrain your freedom

I'm not here to defend bsd licenses though - those are literally cuck licenses
I'm just saying that gpl will hardly do anything
To prevent cancer governments need to impose a free software policy or whatnot, with "open" and "non overengineered" as requirements.
There is no peaceful solution there. Any peaceful solution like gpl won't solve shit in the end even though it may help somewhat sometimes. And even then, I don't think gpl was the deciding factor for google allowing you to flash shit. It's just their marketing strategy for rich xda kids who buy latest phones to flash shit


>they did, case and point the IBM and Microsoft anti trust lawsuits
The 90s were just different. At least current day AmeriKKKa has no issue with the tech monopolies that have formed.

File: 1640293143536.png (237.13 KB, 1920x1404, ClipboardImage.png)


Mass cell production.
Better muon and electron based radars.
Mass production of medical equipment.
Organic prosthetic’s.
Easier access to cancer therapies.
Space robotics for astronaut less exploration.
Computer integrated healthcare treatment.
Computer integrated cities.
Computer integrated heavy machinery.
Industrial robots.
Landing strips for drone delivery.
CRISPR for disease eradication.
Effective Malaria and HIV vaccines.
LRT taking over cars(not new just a future trend).
Better access to treatments for the effects of non pharmaceutical drugs and drug addiction.
1 post omitted. Click reply to view.


>industrial robots for greater productivity, it isn’t automation in the sense that it removes the need to work it just makes current production more productive with more machinery


I like how half this shit already exists or is in development in real life and is far more interesting than sci fi tech garbage spewed by the msm and big tech

Really makes you think about how weird the world really is


Just replace "computer integrated" with "smart" and you have the same thing.


wtf is an organic prostethic?


File: 1643753216873.jpg (230.85 KB, 676x627, 16521616.jpg)

File: 1638599944767-0.png (45.62 KB, 226x223, ClipboardImage.png)

File: 1638599944767-1.png (35.36 KB, 225x225, ClipboardImage.png)


so ive been using e ink shit like kindles and holy shit my eyes dont hurt anymore and i dont feel any headaches. Reading it feels like im reading a regular ass book

so i decided to check computer e ink monitors so to go full e ink and not get eye strain anymore


the first image is 1000 bucks

and the second image is 2000 bucks

8 posts omitted. Click reply to view.


i prefer kobo for the open format and not amazon. But kindle is fine, you just have to convert bookz you pirate iirc




also the latency thing is improving give it time, probably by the year 2035 e ink will rival standard screens


There are screens that can switch between black-white low-energy e-ink and low latency color.


get kindle if you like ads

File: 1642883778792.jpg (4.72 KB, 300x168, download.jpg)


Any info on this? How can I get into semiconductor field? I want to work on the field and help China in having more chips and causing a shortage in rest of the world. US will feel what it is like to be sanctioned.
7 posts and 3 image replies omitted. Click reply to view.


i will short the brains of whoever keeps making prices high


Cryptocurrency was a mistake.


GPU prices aren't a result of mining, they're a result of manufacturers fleecing cuz of the pandemic and them predicting a ton of people with disposable income will suddenly get into building PCs.
I bought a couple of decent modern GPUs for a few hundred each cuz I was building a computer right before the pandemic hit.


GPU prices were skyrocketing before the pandemic. It was 100% because of mining speculators.


>I want to work on the field and help China in having more chips and causing a shortage in rest of the world
one word:


Is open source communism?
6 posts and 3 image replies omitted. Click reply to view.


is alunya in super tux cart now or is that a mod?


File: 1643252791537.jpg (199.72 KB, 1920x1080, 1617329041361.jpg)

Featured add-on in-game.




Not necessarily but copyleft licenses like the (A)GPL do come pretty close. Within the field of course


open source is communism in the degenerate case where commodities completely lack scarcity


haven't seen any talk about OpenStreetMap on here. any other users/contributors?
I like to contribute using StreetComplete when I'm on walks and JOSM when I'm at home and bored
9 posts and 1 image reply omitted. Click reply to view.


>looking at a street and mapping it is datamining
uygha you stupid lmao
>implying there aren't actually beneficial applications using this data


Protip: Don't map your own house without mapping so many random areas. Users can see where you map and when you did it to find where you live.


Did this ever happen to anyone?


>implying I use my real name
>implying I didn't claim to be a little girl
>implying I just map one area
>implying I upload them in real time


I use my amateur radio callsign when mapping, which is easily resolved to my name and address as per regulations
hashtag yolo

Delete Post [ ]
[ home / rules / faq ] [ overboard / sfw / alt ] [ leftypol / siberia / hobby / tech / edu / games / anime / music / draw / AKM ] [ meta / roulette ] [ cytube / git ] [ GET / ref / marx / booru / zine ]
[ 1 / 2 / 3 / 4 / 5 / 6 / 7 / 8 / 9 / 10 / 11 / 12 / 13 / 14 / 15 / 16 / 17 / 18 / 19 / 20 / 21 / 22 / 23 / 24 / 25 / 26 / 27 / 28 / 29 / 30 / 31 / 32 / 33 / 34 / 35 / 36 ]
| Catalog | Home