[ a / b / cf / cy / g / lain / un / pollitx ] [ wired / meta ] [ home / rules / faq / affiliates ] [ mebious ]

/g/ - Technology

Programming and Electronics
Password (For file deletion.)

Mebious now up and running! Access the wired.

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

 No.211[View All]

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


File: 1614371892504.png (17.88 KB, 800x500, 87617512_p1.png)

Here is the program itself:

Definition fib n : { m | fibonacci n m } :=
let aux :=
fix f n :=
match n with
| 0 => (exist (fibonacci 0) 0 fib0, exist (fibonacci 1) 1 fib1)
| 1 => (exist (fibonacci 1) 1 fib1, exist (fibonacci 2) 1 (fibS 0 0 1 1 fib0 fib1 eq_refl))
| S (S n) =>
let (Xa, Xb) := f n in
let (a, Ha) := Xa in
let (b, Hb) := Xb in
let Hab := fibS n a b (a + b) Ha Hb eq_refl in
(exist (fibonacci (S (S n))) (a + b) Hab,
exist (fibonacci (S (S (S n)))) (b + (a + b))
(fibS (S n) b (a + b) (b + (a + b)) Hb Hab eq_refl))
in fst (aux n).

The first line says that fib takes an argument n, and produces such an m, that it is the nth Fibonacci number. (But only a single one and does not say anything about possible other such values.) `exist' is what builds the dependently typed value: its first argument is the property of the value, the second the value itself, and the third is the proof of the property holding for that value. The algorithm is a bit unusual because of Coq's type system. To keep the system logically sound, every algorithm must terminate. In many cases, Coq can automatically detect which argument is decreasing with each recursive call, but in case of the usual recursive definition of Fibonacci, it cannot. With a small trick it can, but that leads to another problem: it must also keep track of `n' to make sure that what it returns is indeed the `n'th number. For this reason both that and the usual iterative version, where it counts from zero up to n, fail type checking because Coq can't establish that the n going in the recursive call and the n coming back are the same.


File: 1616484769382.jpg (68.13 KB, 550x814, cover.jpg)

Anyone else reading SICP2.0? My Scheme skills are a bit rusty but I am really happy to have an excuse to use it again.


Does anyone else keep getting SERVFAIL on DNS requests for wizchan.org?


File: 1617554820348.png (26.86 KB, 720x313, screenshot.png)

idk cause i don't post there but saw this on another board the other day




File: 1617913672356.png (122.3 KB, 529x482, richard_stallman.png)


File: 1618001205173.png (302.39 KB, 1002x405, leah-rowe-defends-stallman.png)

>at the behest of proprietary software vendors
good to see no one's being paranoid about this whole thing


What company would feel threatened by the FSF? They are pretty irrelevant.


File: 1618346622484.jpg (171.17 KB, 1280x720, dumb.jpg)

I'm doing exercise 3.2 right now, and it told me to
> First, make an arithmetic that defines only addition, negation, and subtraction of vectors over a base arithmetic of operations applicable to the coordinates of vectors. Applying any other operation to a vector should report an error.
But if I make it throw an error with `(error "Unsupported vector operation:" operator)', it makes extend-arithmetic fail on zero?. If I return with #f instead of raising the error, it seems to work. I also had to register the `vector?' predicate.

I don't know if I am just not paying enough attention to the text or it really just throws you into deep water with the exercises.


File: 1619125119964.png (7.05 KB, 364x118, Screenshot_2021-04-22_22-5….png)

Finished all the Scheme exercises on exercism. I did most of them around a year ago. Back then it would let you ask for code review on your solutions, which was pretty cool, I learned a few tricks from it. But now it wouldn't let me ask for it, I am not sure why, but it defeats the whole point of the site. Anyway I had it on my todo list, now I can finally cross it out.


I just got into linux lately and I'm still learning basic bash commands lol. So I'm basically just working on being able to properly use a computer. Nothing big but feels good.


That's pretty cool, bash can be really powerful. It's not perfect but it is damn useful.


The GPL license is problematic for the corporate world. Pretty much all proprietary software depends on open source projects and GPL makes leeching off of open source software in proprietary projects difficult. Therefore any organized group that promotes FOSS is a threat. It's all about the money.
I don't know how organized the smear campaign against Stallman was. IMO most likely it was just useful fools who went after him.


File: 1619978291383.jpg (87.72 KB, 300x440, 1387233973349.jpg)

I'm doing the C++ exercises now. They seem to have enough mentors to let me ask for reviews. We will see how it goes, I'm a bit afraid of C++ due to the memes of it being a Lovecraftian horror.


I'm done with the main track of exercises, it was pretty disappointing. It's just 8 exercises and all of them are pretty simple, you don't really need to use any interesting C++ features. There are extra exercises and some of them are pretty interesting, but it's hard to get feedback on those. I'm still doing some of them but C++ is a mess, there's just so much to keep in mind while writing it, I don't think I'll using it in my free time much.


Stallman is his own worst enemy, but his autism made him more effective up until recently.


Does kind.moe seem to be down for anyone else? I keep getting
>Index of /
>Apache/2.4.29 (Ubuntu) Server at kind.moe Port 443


File: 1621491198573.gif (1.82 MB, 360x344, wirechan-on-the-left-kind-….gif)

Yes, it wasn't working at all yesterday and now there's a message that they are working on it. In the meantime you can visit the bunker: https://anon.cafe/kind/


File: 1622800542982.jpg (1.62 MB, 3532x5000, 08992f0f1973102866a332ae43….jpg)

A big thank you for helping out with /kind/!



File: 1622885586667.jpg (26.29 KB, 655x461, 1455647766593.jpg)

Last night I was trying to figure something out but had no success, I couldn't think of anything. So I turned off my computer and started to prepare for bed and of course suddenly all kind of new ideas flooded my head…


File: 1623049902517.gif (1000.05 KB, 495x281, akari.gif)

Looks like the troubles are not over yet…


I don't use anon.cafe due to their captcha/bypass nonsense. Please post the following in https://anon.cafe/kind/res/46.html

>due to excessive CPU usage
You were already told on kind.moe in the thread with 45 replies about the Date and expires timestamps in captcha response headers. Furthermore, in scheduleHandler.js:expiredCaptcha you have:

function expiredCaptcha(immediate) {
if (immediate) {
} else {

schedules.expiredCaptcha = setTimeout(function() {
}, captchaExpiration * 1000 * 1);


Notice the
>captchaExpiration * 1000 * 1
in setTimeout. Never set captchaExpiration to 0.

Separately, from Readme.md:
>* `noReportCaptcha`(Boolean): disables the need for captcha when reporting.


Do you think it is the captcha expiration that causes the excess load? It does not make sense to me, since the client was waiting 256 seconds, does the server just make new captchas without the client side asking for one?


>Do you think it is the captcha expiration that causes the excess load?
It is merely one item to check off the list.

>It does not make sense to me

>does the server just make new captchas without the client side asking for one?
No. The scheduleHandler has an expiration rescanning loop in expiredCaptcha that runs on a timeout of
>captchaExpiration * 1000 * 1
Notice that the callee, checkExpiredCaptchas, ends by handing off to expiredCaptcha again.


File: 1623319069965.jpg (996.58 KB, 1500x1200, calne_ca1.jpg)

I plan on installing Gentoo on a spare machine for the first time in order to learn more about linux.


Exciting! I wish I could Linux for the first time again lol


unless youre getting a job on that field spend that time doing something productive for yourself

Trust me the gentoo rabbit hole its deep


Well yeah, I had the great idea of trying it first time on my nearly 20y/o thinkpad. So compiling the kernel failed after 15hours and 40minutes and I have absolutely no idea what to do about it.
I still don't feel like it was for nothing.

I am about to get a job in this field, but is it really that deep? Everything I heared from Gentoo lately was something like
>Basically the optimization isn't worth it anymore because of fast computers / the compiling time makes it even
>You're already using arch (actually artix) so there isn't that much anymore you're going to learn through getting into gentoo

I thought both were invalid arguments, but it's surprising to hear the opposite.


Should I learn Rust? Is it really going to replace C and C++?


File: 1633346167685.png (24.63 KB, 1071x455, Screen Shot.png)

>Value: 1; The uploaded file exceeds the upload_max_filesize directive in php.ini

when trying to post in >>>/a/12
file size: 2780883
examples of posts over 4MB: >>322 >>324 >>551


Obscure technical searches lead me to underground chans. nice to know you all continue to exist. please keep allowing indexers to crawl you so this will happen in the future, thank you.


Welcome, friend.


Can we get an admin answer to >>746 ? Is it misconfiguration or has the file size limit been lowered?


Filesize limit was lowered.



File: 1642225305015.jpeg (866.37 KB, 1920x1200, the binaric machine.jpeg)

working on self-teaching myself the workings of the computer. I've pirated a bunch of textbooks, and have a few projects in mind. Wish me luck.


Goodluck, what kind of project(s) did you have in mind?


mostly making stupid applications. somethings for automating some TTRPG processes, and something like a program that place customizable virtual waifu assistants on your desktop (which I think exists already). The big goal is to learn how to white hat properly while doing small software projects to avoid psychosis. Also it's good programming practice.


if you would like to make a study group on this board I would be amenable to joining and going through your textbooks
although I would request to see the titles you're going through first


File: 1642481757482.png (972.64 KB, 1280x720, structure and interpretati….png)

sure thing Anon, though, to create that study group board, I think I'd need to progress further with my studies than where I currently am (I started just as I wrote that post). The books I've got lined up for reading are:
>Compilers: Principles, Techniques, and Tools (The Dragon Book)
>Computer Networking: A Top-Down Approach (6th Ed)
>Computer Systems: A Programmer's Perspective
>Crafting Interpreters
>Designing Data-Intensive Applications: The Big Ideas Behind Reliable, Scalable, and Maintainable Systems
>Mathematics for Computer Science (Eric Lehman)
>Operating Systems: Three Easy Pieces
>Structure and Interpretation of Computer Programs (2nd Ed)
>The Algorithm Design Manual
The list isn't in any particular order, and the book I'm on right now is SICP


File: 1642551673388.png (983.27 KB, 1258x1374, 1879234572345.png)

Thanks for the comprehensive list. A good portion of them seem interesting.
Especially the lower level stuff.
I don't think I'll be following along with SICP.. Reading some CL stuff instead.

On Lisp in particular.

Here's a link for anyone interested in SICP though. The formatting is nice.

If you get anything out of SICP, I would like to know. I'm just going to put it off for now.
Not convinced Scheme is the way forward


>especially the lower level stuff
I should've mentioned I'm starting from near zero here. Besides some codemonkey experience in Python, C, and Lua.
>If you get anything out of SICP, I would like to know.
I'll keep you posted Anon!


SICP is not about Scheme, it doesn't even cover the full language. You will learn a lot from it even if you never use Scheme ever again.


I skimmed the book further due to your suggestion. For a good hour or so.
It covers a lot of interesting computer concepts, most I am familiar with due to previous compsci books and lisp books.

>It was formerly used as the textbook for MIT's introductory course in electrical engineering and computer science

So it doesn't seem practical to me, but it is a great introduction. Would definitely be practical for others.
I've never took the time to go through the ToC and jump around the chapters to make this conclusion before.

It would've been nice to have this as my introduction to computation, but oh well.


I'll consider myself lucky to have it as my introduction then!


Is textboard.org down?


File: 1644053720887.png (29.55 KB, 200x193, works-on-my-machine.png)


Thanks. Now it's back for me too, just super slow.


Is anyone else getting captchas when trying to search for anything on:

[Return][Go to top] [Catalog] [Post a Reply]
Delete Post [ ]
[ a / b / cf / cy / g / lain / un / pollitx ] [ wired / meta ] [ home / rules / faq / affiliates ] [ mebious ]