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

/g/ - Technology

Programming and Electronics
Name
Subject
Comment
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

What are you working on, /g/?

 No.216

I'm really sorry about textboard.org but Bitdiddle said the stress tests were badly needed and kept encouraging me. I hope it's back up soon.

 No.217

File: 1582269064422.jpg (160.42 KB, 800x998, marika_kato__bodacious_spa….jpg)

>>216
It seems to have returned from death.



Why are you testing in production?

 No.218

File: 1582283674971.jpeg (168.42 KB, 1000x1358, 4798701.jpeg)

>>217
>Why are you testing in production?
Setting up a local copy is such a hassle and Bitdiddle said:

>Don't worry about that. I'm sincerely grateful you found that severe bug, took the time to read the code and offered a way to fix the issue


>We badly need those. Now is the time.


>Thank you again for discovering that awful bug. I believe your stress tests will hit the nginx cache, so they should be safe.

 No.230

File: 1583269287742.png (1.42 MB, 900x1200, 1567550669432.png)

I am trying to change a pretty fundamental type in a functional program, as the current one turned out to be inadequate… Hopefully I won't end up having to rewrite the whole thing. How do functional programmers deal with cases like this? Just get it right before beginning?

 No.232

File: 1583344027901.jpg (38.38 KB, 249x332, capable.jpg)

>>230
Looks like I managed to avoid the situation. Though I am still curious how people deal with situations like that.

 No.257

Currently implementing truth tables for propositional logic in Python. I am aiming to make it general enough so that I can represent every possible table (not just AND, XOR and the usual) with any number of truth-values.

Fun fact: if you have V truth values, then the number of possible truth tables for a binary connective (a truth table with two inputs, basically) is: V ^ (V ^ 2).

This number gets very big very quickly:
V - V ^ (V ^ 2)
1 - 1
2 - 16
3 - 19683
4 - 4294967296 (4.3 billion)
5 - 298023223876953125 (298 quadrillion)

 No.258

>>257
>with any number of truth-values
What are you going to use for not(not(x))?

 No.260

File: 1586901531346.jpg (7.52 KB, 183x275, Curious Miku.jpg)

>>230
What exactly were you trying to do?

 No.261

>>258
Aha. My impression is that NOT(NOT(p)) has the same truth value as p in most many-valued logics, especially those with a finite number of truth values. The Wikipedia article will give some examples:
https://en.wikipedia.org/wiki/Many-valued_logic

The program I'm writing won't be able to handle intuitionistic logic, where NOT(NOT(p)) =/= p, because intuitionistic logic does not use truth tables. At least, it doesn't use finite ones.

 No.262

File: 1586975322394.jpg (733.39 KB, 1000x1300, 7cabe45a4f8164a082f778b9b5….jpg)

>>260
It was an interpreter-like program where certain escape sequences were handled on the parsing side, but I needed to preserve them for later use. I ended up encoding them in the AST using already existing constructs but it's ugly and the proper way would be to change the AST. I know that the whole thing sounds horrible but believe me, it is actually much worse.

 No.286

File: 1589832842137.png (2.01 MB, 620x850, Generaltan.png)

I am giving Coq another go, this time using Programs and Proofs: https://ilyasergey.net/pnp/

I expect to lose track of what is going on somewhere around the middle of the third chapter.

 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.

 No.317

File: 1591988277700.png (337.88 KB, 792x720, 1450102382233.png)

>>286
I am really glad I started reading this, Coq is lots of fun.

 No.321

File: 1593463036175.jpg (614.33 KB, 1200x1680, 44ac5083e0a37d3fede1a06570….jpg)

>>286
I finished this. I liked it a lot, although the last chapter maybe progressed a bit too quickly, I ended skipping most of the exercises there. Maybe I will return to it someday.

Should I continue with Software Foundations or should I try The Little Prover before it?

 No.322

File: 1593682205757.jpg (4.25 MB, 2254x3200, badgateway.jpg)

Can anyone post on textboard.org? I have a bug report and fix to post and I keep getting 502.

 No.323

File: 1593703931946.jpg (1.4 MB, 1103x1826, 15e8f3fbb248eb1faf2bec4f47….jpg)

>>322
I get 502 too… maybe you could post here instead? What are you working on, textboard engineering?

 No.324

File: 1593720787662.jpg (4.14 MB, 2244x3706, image.jpg)

OK, it's back up.

>>323
>What are you working on, textboard engineering?
Nothing so lofty. I'm just contributing in my small way to the SchemeBBS community by providing bugfixes.

 No.325

File: 1594070761376-0.jpg (163.12 KB, 661x920, 1588027855042-prover.jpg)

File: 1594070761376-1.jpg (162.44 KB, 661x920, 1588027855042-sicp.jpg)

>>321
Wow I thought The Little Schemer will be some quick enjoyable read, but it is quite laborious. It took me a while to figure out how to follow along with the code as the instructions are not very user-friendly. I use "J-Bob/step" for the actual proving and only copy it into the proper "J-Bob/define" once it is done. It is pretty fun though and I am looking forward to reading the actual implementation too. It is just a bit too manual after Coq, you have to type a lot!

 No.326

File: 1594320697293-0.gif (706.24 KB, 1280x1086, 90401bed27c927690db68bf6ee….gif)

File: 1594320697293-1.png (7.02 KB, 734x25, Screenshot_2020-07-09_20-4….png)

I'm hacking on some Scheme code and noticed this… Thank you Geiser, very useful info.

 No.328

>>325
I finished it but I am not satisfied. It could have had more examples on the main techniques, like how to construct the totality claims and such. It did not feel like by the end I understood the main principles, if there were any.

 No.329

File: 1594568499786.png (165.13 KB, 510x346, Nichtskapiert.png)

>>328
Actually, thinking about it a bit more, I think I get it now.

 No.330

>>211
On my personal website.
>https://kamel.surge.sh

 No.331

>>330
Nice little website, good job!

 No.332

>>331
Thanks :D

 No.333

The SchemeBBS "fossil repositories" link gives
https://fossil.textboard.org/
502 Bad Gateway
nginx/1.18.0

Posting in the sandbox gives
https://textboard.org/sandbox/1
error 502
bad gateway

Anyone else seeing this?

 No.334

>>333
Nice repeating digits. Yes, for me everything dynamic gives 502 error, even viewing individual posts like here: https://textboard.org/sandbox/1/1

 No.335

File: 1595113198153.jpg (658.87 KB, 900x1273, t.jpg)

>>334
Thanks for the confirmation. Hope it's back up soon.

 No.336


 No.343

File: 1595789829717.png (444.99 KB, 1280x720, 1595728207571-sicp.png)

I started reading the first volume of Software Foundations, Logical Foundations. It's pretty nice so far, but today I did nothing but the pumping exercise in the IndProp chapter and I still did not manage to finish it. I just can't figure out the App case. I already did every other case but this one just seems impossible.

Maybe I should be working on some project instead of always just reading.

 No.346

File: 1596142644191.png (10.36 KB, 855x855, 0b447a826e8900385d59db99a4….png)

>>343
I get too engrossed and spend all night playing with my Coq. This can't be healthy! I managed to figure out the pumping lemma but now I am stuck on palindrome_converse and can't progress at all. I need induction on (l = rev l) but of course the usual list induction won't do it, because (h :: t = rev h :: t) does not mean (t = rev t).

 No.349

File: 1596573228860.png (185.08 KB, 600x600, cc02bcb0378c60a175e8483b85….png)

>>343
>>346
I'm proud to announce that I have finished that chapter. If I continue progressing at this rate I might finish the first volume by the end of the year!



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