[ a / b / cf / cy / g / lain / un ] [ fresh / meta ] [ home / rules / faq ]

/g/ - Technology

Programming and Electronics
Name
Subject
Comment
Verification
File
Embed
Password (For file deletion.)

Hop in to our IRC channel! #wirechan@rizon.net

File: 1581460038602.png (503.48 KB, 934x1000, daily_programming.png)

 No.211[Reply]

What are you working on, /g/?
11 posts and 7 image replies omitted. Click reply to view.

 No.287

>Coq
>Lego
>Isabelle
You forgot to add TypeScript.

 No.291

>>287
What do you mean? If this is a joke, I don't get it.

 No.292

>>291
It is. You'll get it when you're older.

 No.302

File: 1590733791715.jpg (1006.46 KB, 1214x1805, 5389b33aa21c88bc7304f934cc….jpg)

>>286
As expected, it was progressing a bit too fast for me. Before continuing on to chapter 4, I am reading this tutorial: https://mdnahas.github.io/doc/nahas_tutorial

I like that it uses only the most basic parts of Coq and explains them in terms of the Curry-Howard correspondence. It makes me want to write my own proof assistant!

 No.315

File: 1591127549558.jpg (311.75 KB, 2400x3200, 59f557afe19fe20741c3e75c9c….jpg)

Is there a better way to repeatedly destruct a hypothesis so that it can be handled in one go like here?

Goal forall n, n = 0 \/ n = 1 \/ n = 2 \/ n = 3 -> n - 3 = 0.
intros n Cs.
destruct Cs as [C|Cs]; try destruct Cs as [C|Cs]; try destruct Cs as [C|C];
rewrite C;
reflexivity.
Qed.

I guess "repeat" would kind of work, except for the last one where the naming wouldn't match.



File: 1553638781535.png (58.25 KB, 220x203, 220px-Gnu-and-penguin-colo….png)

 No.83[Reply]

What got you into Linux?
33 posts and 2 image replies omitted. Click reply to view.

 No.282

>>259
>And I don't feel like using WSL.
As someone who uses it for work - WSL is surprisingly non-awful. And having a decent shell and utilities around makes Windows much more tolerable.

 No.283

The Godot (game engine) discord server had a room where people would post RMS memes. They also had the command .rms.

So one day I was curious and watched a talk of RMS.
And because I'm rational, I could see how objectively everything this man was saying made sense.

Became free a few weeks after. Never looked back. Best choice of my life.

 No.311

>>282
Embrace, extend, and extinguish

 No.312

>>311
We are already at the extend phase.

 No.314

>>83
Windows



File: 1566843455180.gif (1023.34 KB, 500x500, floating-point.gif)

 No.144[Reply]

Have you ever operated a chan?

What does it take, in terms of memory, CPU, bandwidth and disk space to run a chan? Let's suppose it's at wirechan's posting rate.

What software is best? Vichan? Lynxchan?
23 posts and 3 image replies omitted. Click reply to view.

 No.304

>>299
>my backwater boards.
Stop pretending you're some leet hackers in the cyberspace. Ironically, so many lain followers are full of themselves that you can't grasp the full meaning of the show

 No.305

>>300
You were saying how you rolled your own.
>>303
There's nothing better to do here but to reply to bait. Nobody really cares about this place.
>>304
Nice projection. Nobody likes it when shit is shilled. Being an imageboard doesn't mean free speech extremism. I don't even like lain. Are you a laincel?

 No.307

File: 1590834340846.jpg (2.42 MB, 3508x4961, sword.jpg)

>>305
>I don't even like lain.
Come say that to my face, motherfucker!

 No.309

>>305
Nothing wrong with a little shilling every once in a while
>I don't even like lain. Are you a laincel?
Why don't you like lain? I enjoyed the the show and the topics that it introduced, like surveillance and the wired. I thought this was a technology and anime imageboard. Theres even a Lain board. Is she too loli for you?

 No.313

File: 1590959264175.jpg (27.99 KB, 322x453, you.jpg)

all you guys are faggots and losers and a are ruining backwater boards with your autistic/incel/neet/ shit it was never about that

your identity is fucking anonymous stop powerleveling and spilling your life all over the internet


>>305
>I don't even like lain.
MODS ban please thats like going to an IRA meeting and praising the english



 No.308[Reply]

How are these videos made? It looks like some kind of animating software and not hand drawn, right?

 No.310

Freaky. I think they draw a couple images and use animation to fill in the rest



File: 1576073341839.jpg (516.95 KB, 676x842, 1384493133443.jpg)

 No.161[Reply]

Lainchan and Arisuchan are full of idiots now, and 4/g/ is out of the question. But this imageboard could use some activity, any ideas?
20 posts and 3 image replies omitted. Click reply to view.

 No.223

>>222
lainchan decline era user detected

 No.263

>>222
people like you are the reason there are millions of small imageboards instead of a couple of big ones

 No.265

>>170
lainchan is being killed by mods who throw warns in every possible direction and remove anything they personally do not like. And since walls of text about politics, drugs and gay shit don't touch their feelings, this is exactly what you will see. Because for generating any other kind of content - even by creating a desktop thread, where title speaks for itself - you get warned for being "not informative enough", or your post gets removed.

>>222
I'm personally tired of shitposting. Meta-shitposting is fine since at least it is something new and unique, limited to one little community, it develops its culture. Seeing the same kinds of posts with le funi memes over and over again is tiring.

 No.266

>>265
lainchan was on its last legs since the arisu split, then after "small" imageboards became cool it was the most targeted one since it was the best one, a while later a the fall of 8chan brought all the stragglers were looking for an alternative because the other boards suck(including 8chan) not realizing they are the reason that it sucks and whenever they go they will bring the decline with them.

>>178
this thread makes me physically sick

 No.306

>>222
>I feel like there isn't enough space for shitposting.
I feel like the internet has enough space for anonymous shitposting as it is.



File: 1581156554049.png (789.07 KB, 761x1066, 86532c04290d84566673d48110….png)

 No.206[Reply]

With the GPL, for any binary that you distribute, you have to make the corresponding source code available. With reproducible builds (see: https://reproducible-builds.org/), it is possible to verify that the binary was indeed compiled from the available source code. All you have to do is to compile the source code yourself, and compare the resulting binary with the one distributed. For an example of this in practice, see guix's `challange` command.

With the AGPL, if you run a service accessible through a network, you have to make the corresponding source code to the service available to the users. But is there a way for the user to verify that the service provided corresponds to the source code available? I can't think of any situation where the service couldn't just simply lie about what it is.

 No.207

Try asking on textboard.org maybe.

 No.208

>>207
Is my thread not welcome here?

 No.210

File: 1581359975763.jpg (73.11 KB, 850x1200, 994779f8f513495c26788a9ebb….jpg)

I believe this to be very important in today's climate where every megacorporation tries to paint themselves to be great supporters of "open source" and many of our organizations are funded by their "generous donations". But the problem is that they don't give a shit about software freedom. Take Visual Studio Code for example. Microsoft used to advertise it as being Open Source, and millions in good faith downloaded binaries of it. Until a careful eye noticed that the source code released as "Visual Studio Code" was different from the binaries released as "Visual Studio Code". In fact, the binaries even have their own license agreement that you have to accept to use them. After being called out on it, Microsoft modified their website and now Visual Studio Code only claims that it was "built on Open Source", as if that was something to be proud of. But the damage has already been done. I think Docker employed (or still employs) similar tricks. The problem is, pushover (so-called "permissive") licenses do not protect you from this trickery at all. With copyleft licenses, the source code of the binary has to be provided. But with pushover licenses, corporations can put some crippled version of their software on Github as bait, and distribute proprietary versions of it in binary form. This is why I think verifying source-to-binary correspondence, enabled by bootstrappable and reproducible builds, is so important.

 No.295

File: 1590608259919.png (210.98 KB, 1102x826, slide 18.png)

>>210
https://media.libreplanet.org/u/libreplanet/m/the-four-free-ums/
There was this talk at LibrePlanet 2020 by someone from the Open Source Initiative(!) about some current practices that companies employ to appear as part of the Free Software movement without actually adhering to the principles of software freedom.



File: 1516668980885.png (364.07 KB, 1920x1080, zJkdm1n.png)

 No.9[Reply]

Netrunner thread

 No.11

>>9
It's still alive?

 No.285

>>11
sadly no

 No.290

The browser, the distro, or the card game?



File: 1530626857014.jpg (74.64 KB, 829x613, 52528994_p0_master1200.jpg)

 No.37[Reply]

What is the worst thing ever happened on your PC?
32 posts and 6 image replies omitted. Click reply to view.

 No.203

>>199
>I used to regularly thrash my HDD by distrohopping and overwriting it with a new OS every 1-2 weeks.
How does that work? A distro install isn't a lot of data, so one every week can't add much to your average write rate.

 No.204

>>203
I never bothered with thumb drives much, usually because I didn't have one around most times, so I had a separate partition on the disk that I wrote the ISO to which I would boot from. From there I would install whichever distro to the rest of the disk. I basically was writing 3 separate copies of the distro iso/files to the same disk every time I hopped.

 No.256

>be 8
>Wanted to make stupid stick figure animations with lazer effects
>thought Macromedia Flash was free software so I googled it
>literal site I stumbled upon had a “THIS DOWNLOAD MAY HAVE A VIRUS” banner
>download anyway
>thousands of error messages
>smash that motherfucking like button for 00’s internet

 No.288

>>256
I went through something similar XD

>be me, 9 years old

>get a cheap Dell laptop for Christmass
>AwYeah.jpg
>Immediately search up "Minecraft for free"
>go to the first website, already looking sus
>download it without a second thought
>computer becomes very slow for some reason
>see that I have a new app with a pink dolphin logo
>coolbutididn'task.png
>didn't get minecraft for free but I got a lot of popups of sexy gurls on every webpage ;)

We all learn about internet safety eventually…

 No.289

>>37
>What is the worst thing ever happened on your PC?
Me.



File: 1581665730308.jpg (153.2 KB, 1348x900, ilovefs-gallery-136.jpg)

 No.212[Reply]

Do you love Free Software? Let's share some Free Software that we love!

 No.213

Yeah boys. some of my (free || open) source software

1. OSs: Debian, Void, Plan9, & OpenBSD
2. Editors: Acme, Emacs, & Sam

W8.
Here is a list:
https://github.com/mayfrost/guides/blob/master/ALTERNATIVES.md

 No.214

File: 1581836737405.jpg (22.84 KB, 480x360, 1464840777557.jpg)

>>212
I wish I could find a cute gf that's into free software, a good OS, and hates smartphones.

 No.215

I am really glad that Anki exists. It saved me from failing out of university.

 No.284

>>213
include gentoo



File: 1589118586436.png (200.87 KB, 652x343, 4bba512cacbc14d7e081cf1e43….png)

 No.271[Reply]

Would it be possible to have a programming language that is not based on English reach mainstream adoption?
1 post omitted. Click reply to view.

 No.273

The world isn't that cool anymore. At best you'd get something out of China. Scary if they win the AI race.

 No.274

File: 1589266235358.jpg (256.26 KB, 2466x2119, 46b28ab8221945df9cb5542f9a….jpg)

>>272
How about something like APL that manages to avoid the language question altogether?

 No.277

>>274
why would people want to go back to hieroglyphs?

 No.280

File: 1589394544127.jpg (884.85 KB, 960x1280, 81197493_p0.jpg)

>>277
Same reason they use them in maths? Why should programming languages mimic human languages when programs do not behave in any way resembling human thoughts?

 No.281

File: 1589428023532.jpeg (56.66 KB, 312x537, jason.jpeg)

>>280
because humans make it and use it, the machine doesn't care you can make a language based on different dick sizes and it will still take it, but we don't think like that we think and verbalize our thoughts with words, we refined to a point where we can use letters who are easy to grasp and to memorize in a verbal way who can also be used in a number of different variations

square+circle+lain+circle+dildo+triangle= function a
"a" = function a



Delete Post [ ]
Previous [1] [2] [3]
| Catalog
[ a / b / cf / cy / g / lain / un ] [ fresh / meta ] [ home / rules / faq ]