/g/ - Technology

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

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

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

>>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!

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.

>>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.

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.

>>282
Embrace, extend, and extinguish

>>311
We are already at the extend phase.

>>83
Windows

>>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

>>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?

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

>>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?

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

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

>>222
lainchan decline era user detected

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

>>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.

>>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

>>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.

Try asking on textboard.org maybe.

>>207
Is my thread not welcome here?

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.

>>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.

>>9
It's still alive?

>>11
sadly no

The browser, the distro, or the card game?

>>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.

>>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.

>>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…

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

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

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

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

>>213
include gentoo

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

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

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

>>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?

>>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