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

/g/ - Technology

Programming and Electronics
Password (For file deletion.)

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

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


What are you working on, /g/?


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.


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

It seems to have returned from death.

Why are you testing in production?


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

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


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?


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

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


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)


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


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

What exactly were you trying to do?


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:

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.


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

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.


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.


You forgot to add TypeScript.


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


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


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

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!


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;

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


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

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


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

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?


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.


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

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


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

OK, it's back up.

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


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

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

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!


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.


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.


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

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


On my personal website.


Nice little website, good job!


Thanks :D


The SchemeBBS "fossil repositories" link gives
502 Bad Gateway

Posting in the sandbox gives
error 502
bad gateway

Anyone else seeing this?


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


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

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



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.


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

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


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

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 ]