What are you working on, /g/?

Name
Subject	Spoiler Image
Comment
File
Embed
Password	(For file deletion.)

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

Daily Programming Thread Skyglider 02/11/20 (Tue) 22:27:18 No.211

What are you working on, /g/?

Zodiac 02/21/20 (Fri) 00:06:17 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.

Daphne 02/21/20 (Fri) 07:11:04 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?

Cracky 02/21/20 (Fri) 11:14:35 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.

Anonymous 03/03/20 (Tue) 21:01:27 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?

Guest 03/04/20 (Wed) 17:47:07 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.

Skyglider 04/12/20 (Sun) 00:30:36 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)

AzureDiamond 04/12/20 (Sun) 09:40:59 No.258

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

Virtual Ghost 04/14/20 (Tue) 21:58:51 No.260

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

>>230
What exactly were you trying to do?

Guest 04/14/20 (Tue) 22:11:16 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.

Daphne 04/15/20 (Wed) 18:28:42 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.

Cidoku 05/18/20 (Mon) 20:14:02 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.

Skyglider 05/19/20 (Tue) 09:42:26 No.287

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

Cidoku 05/23/20 (Sat) 20:58:33 No.291

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

Shenzen 05/24/20 (Sun) 09:32:05 No.292

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

AzureDiamond 05/29/20 (Fri) 06:29:51 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!

Observer 06/02/20 (Tue) 19:52:29 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.