The Nineteenth Byte

Adám

00:00

@cairdcoinheringaahing Thank you for that feedback.

New Posts

0

Q: Lean golf: Pascal vs. Fibonacci

The Pascal's triangle and the Fibonacci sequence have an interesting connection: Source: Math is Fun - Pascal's triangle Your job is to prove this property in Lean theorem prover (Lean 3 + mathlib). Shortest code in bytes wins. import data.nat.choose.basic import data.nat.fib import data.list.de...

New Loophole Proposal

00:18

1

A: Loopholes that are forbidden by default

Sidestepping in a theorem-proving challenge A theorem-proving challenge is about proving a statement (= constructing a value of the given type) given in a specific host language (designed for theorem proving, most likely Lean or Coq). One problem with this is that the host language may have vario...

OldSandboxPosts

01:00

Sandbox posts last active a week ago: How many values of this type?

AviFS

01:24

@Bubbler Doesn't it make sense to expand the scope of the question to all langs capable of proving things. Of course, different ones begin with different assumptions, but supposedly competition is only between languages. So I can't see that it would take anything away from all the LotMers to allow other langs for the lean challenges.

lyxal

userinyerface.com

the first page requires a password with a cryllic character

the fools didn't count on me having many ways to quickly get unicode characters because golfing languages

AviFS

It doesn't seem different to me from allowing different langs to compete in code-golf. One could, of course, say some langs "import" more things for free. Eg C++ always has to import iostream, whereas Python gets print "for free." Isn't getting functions for free the same in spirit as other theorem-provers getting axioms for free?

Unrelated String

@Adám cube apple is great, parallel lines/ligature/quad all hurt my eyes, and the rest are nice

lyxal

I like cube apple the most

Unrelated String

@lyxal imagine not having a russian keyboard profile for typing flashcards

Adám

01:28

@UnrelatedString @lyxal Thanks for the feedback.

Unrelated String

i feel like the two strongest points of the cube apple aside from the cube apple itself are the symbol-resembling font of the text and the way the cube is shaded; they give it a modern but distinctive feel

AviFS

@lyxal Is it possible to finish or does it keep cycling through captchas?

Oh... you have to select all of them facepalm

06:37

Bubbler

@AviFS It has been already discussed here (also see my comment there)

AviFS

@Bubbler Ah thanks, I hadn't realized; I'll check it out!

Wait, but the justification here is:

> I do think that any of these challenges would be significantly worsened by attempts to make them language agnostic. They would have to be very complex in their definitions, making a bloated challenge that's only really fun in one or two languages anyway.

The particular challenge you posted seems trivial to formalize in a language-agnostic way, by which I mean with mathematical notation. Actually, the math would be much simpler than that used in loads of problems on CGCC

And on top of it, I think that formalization would actually be much easier to read for most than the Lean code you posted. No?

Bubbler

01:47

1. You need to define what a proof is in language-agnostic way. Can you? I tried but failed.

AviFS

You know way more about theorem-proving challenges on CGCC than I do, Bubbler. I'm just jumping into the deep end!

Bubbler

2. Even if we restrict to known theorem-proving languages, the necessary definitions to form the statement must be presented per language (and the writer should make sure that the definitions actually work as intended), which is only an extra hassle to the challenge writer

lyxal

@AviFS haha it took me 3:32

@AviFS yeah that got me too

AviFS

I know you guys have been trying to make good theorem-proving challenges for way longer than I've been here. I don't mean to question you guys!

@lyxal I finally got it for the "glasses" one, haha

Bubbler

You just questioned our decisions though

AviFS

01:52

Right, I know! But like, an innocent question. I just wanted to clarify that I know you guys have put a lot of energy into this and I'm just jumping in, because it seemed like the answer was involved and I didn't mean for it to be taken personally like at all. And I couldn't tell if you were! Communication can be really hard over text!

Redwolf Programs

4:41

AviFS

The fact that you used bold, added a number one at the beginning, and then said "Can you? I tried but failed" made me wonder if the question was taken as imposing!

lyxal

@RedwolfPrograms get good

AviFS

So have we never had successful language-agnostic theorem proving challenges before, then?

Bubbler

We never had one, except for proof-golf which were about proving something without using any language

AviFS

01:57

@Bubbler Those I've seen! Well I can definitely do a bit more digging on the meta then, and maybe wait until I have something put together to propose before poking at the challenge

Note to self: We should spotlight this answer for one of the yearly things.

It's a very hard question and there are only two answers. The older one has 28 upvotes, but the newer and winning one, by far, has only 3 (now 4).

Bubbler

Nah, it wasn't written in 2021, so it doesn't qualify for yearly best of

You can propose as an underappreciated answer here though

@AviFS If you're thinking about listing Lean's axioms and asking for a proof-golf, please don't. The logic of CIC (calculus of inductive constructions, the basis of Lean and Coq) doesn't fit in one page and it takes forever to derive anything interesting from the ground up

Sandbox Posts

03:38

0

A: Sandbox for Proposed Challenges

Lean golf: List Game (rev_rev) The title is an homage of the Natural Number Game, which is a nice interactive tutorial into proving certain properties of natural numbers in Lean. Given that the previous two were slightly too involved (either mathematically or technically) for newcomers to Lean (i...

AviFS

03:54

@Bubbler Yeah, thanks that's what I meant!

@Bubbler Definitely wasn't even thinking of considering to do that! Thanks though, haha. I'm thinking about asking for a proof without listing any axioms at all, and then seeing where different mathematical systems and proof techniques/langs take it. I don't know if it'll work but those are the lines I was thinking along.

Bubbler

Proof without axioms is way too broad. Every mathematical theory needs to start somewhere (natural numbers start with Peano's axioms, for example)

hyper-neutrino

is it even possible to prove anything without axioms?

doesn't incompleteness prevent that or am i remembering things wrong

Bubbler

And if you can assume arbitrary axioms, how would you prevent people from taking the task itself as an axiom?

@hyper-neutrino I mean, proof without (fixed set of) axioms

hyper-neutrino

ah

caird coinheringaahing

Only on SO

Bubbler

04:04

Gold = Bronze + Silver (almost). That's... crazy :P

caird coinheringaahing

Honestly, I doubt that anyone could legitimately complete 211000 reviews competently

Bubbler

Agreed

Redwolf Programs

It's SO, if you're providing useful feedback instead of downvoting and moving on, you're doing it wrong :p

Throw in some canned comments if you're feeling extra

caird coinheringaahing

It feels bad to single out this user, but I genuinely believe that the top reviewers on SO, at least sometimes, use robo-review scripts

Redwolf Programs

Idk, 211000 is probably less than it seems on a site with as many review tasks to do as SO

If you take 20s per review task, that's just 48 days straight of reviewing

Which is a lot, but divided over several years I could see that being possible

And I'd think after 200k, any patterns caused by robo-reviewing would've been spotted

caird coinheringaahing

04:10

Wait

It's been "today" for 4 hours so far, and each queue has a limit of 40 reviews. So how does this user have 80 already?

Redwolf Programs

It appears the limit is 80 for them

pVC aecidiospore adduced

@RedwolfPrograms do you have Divisions in biology / physics / geography/ computer??

Redwolf Programs

Bubbler

That link redirected to a regular review task for me, and it shows "Your daily reviews 0 /80" for me

hyper-neutrino

yeah when i go to the queue, at least FQ shows the limit is 80

caird coinheringaahing

04:12

I got the link wrong, then corrected it btw

Redwolf Programs

@pVCaecidiosporeadduced ~~No, we only do division in math class~~

hyper-neutrino

yeah all are 40 except LQA, LA, and FA are 20, and FQ is 80

caird coinheringaahing

Also, this [faq] on MSE needs updating

@hyper-neutrino Hmm, forgive my suspicion for a user having already hit the limit, when the next highest is 39

Bubbler

So many queues :P

Redwolf Programs

@RedwolfPrograms Where I am, all of those are separate classes (Biology / Biology AP, Physics / Physics AP, World Geography / Human Geography AP, Computer Science A AP)

hyper-neutrino

04:14

@cairdcoinheringaahing yeah, it looks very weird on first glance to me too :P (for me, the next is 40, which is exactly the limit i thought they had lol)

caird coinheringaahing

I cannot see anything here mentioning raising the limit to 80

hyper-neutrino

might just be SO-specific

all of ours seem to be 20 (although except during the height of our activity i don't think we've ever even generated 20 tasks in one queue in a day)

caird coinheringaahing

@Catija Can you confirm whether the limit has been raised to 80/day and if so, in which queues? I literally cannot find anything relevant searching for "[review] 80" on MSE

Bubbler

I found a reference here on MSO

which was posted less than a day ago

Redwolf Programs

I love how Spanish's "miles de kilómetros" looks like it'd mean "miles of kilometers" :p

Bubbler

04:20

> The daily review quota has recently been increased from 40 to 80 for just the First Questions Review Queue, and only when the queue has more than 1000 items in it.

caird coinheringaahing

@Bubbler I shoulda waited a few seconds as not to ping Catija :/

Bubbler

It's somewhat like SO runs a different software from the rest of the network

pVC aecidiospore adduced

@RedwolfPrograms whats that AP?

Redwolf Programs

Advanced Placement

Basically for us, we're required to take at least four math, science, and history classes (plus other stuff, of course) in order to graduate. So things like biology and physics are year-long science classes specific to that subject. Same with history (they group geography in with that). Computer science is a bit different, since it's not required.

lyxal

@RedwolfPrograms how long do you have left until you graduate from school?

Redwolf Programs

04:29

I'm in 10th grade now, so just over two and a half years.

Unrelated String

i have never been able to think of you as that much younger even though i feel you've mentioned it before

5

Redwolf Programs

It's okay, I'm going to catch up to y'all soon then we can all be the same age together

pVC aecidiospore adduced

> Movement of the earth on its axis is called as Resolution

lyxal

duh

why else do you think they're called New Years Resolutions /s

Razetime

@RedwolfPrograms just go to that one beach which makes you old

AviFS

04:41

@Bubbler Programming without primitives is way too broad :p

@Bubbler And if you can assume arbitrary primitives, how would you prevent people from using/writing an esolang where the task itself is a primitive

Redwolf Programs

Oh hey, tomorrow's friday already

See y'all then o/

AviFS

@pVCaecidiosporeadduced Supposedly it means it's a college level class in the States. In my experience, college classes are way easier ; )

Razetime

@RedwolfPrograms cya

pVC aecidiospore adduced

Aaroneous needs to wait 3 hours before i give him 50 rep

why the 3 hours?

hyper-neutrino

bounties can't be started within i think it's 48h if that's what you mean

Bubbler

04:47

@AviFS We don't prevent it, we just say "please don't, it's boring"

AviFS

It was a rhetorical question, though!

Bubbler

Well yeah, I got that, but still

AviFS

I don't know that it'll work. Not by a long shot. But one can hope that some of the same norms & upvoting logic will carry over

caird coinheringaahing

05:15

@UnrelatedString Ikr, the fact that Redwolf is 3 or 4 years younger than me is O.o

lyxal

wait 3 or 4?

dang

I thought Redwolf was only 2 years younger

caird coinheringaahing

Also, in case anyone is wondering why I'm awake at 6am, its because, until literally 10 seconds ago, the parking garage across the road from me has had its fire alarm running non-stop since 10pm

@lyxal IIRC Redwolf is either 15 or 16

lyxal

@cairdcoinheringaahing oof. You don't have earplugs/noise-cancelling headphones/etc?

caird coinheringaahing

I have noise cancelling headphones, but I can't wear them when I sleep

lyxal

Wait fire alarm? Did no one else think to do something about it?

caird coinheringaahing

05:19

@cairdcoinheringaahing Oh, I was wrong. They haven't stopped it, they're just running it at on/off intervals of around 30 seconds

@lyxal Nope

pVC aecidiospore adduced

[>+<-]

caird coinheringaahing

I live next to a police station as well, nothing from them either

pVC aecidiospore adduced

if bf had variables that store code

caird coinheringaahing

Isn't that just a function?

lyxal

@cairdcoinheringaahing but surely you're not the only one who had their sleep disturbed by the fire alarm.

pVC aecidiospore adduced

05:21

@cairdcoinheringaahing y..yes

caird coinheringaahing

@lyxal I'd imagine not

pVC aecidiospore adduced

06:52

time for geography exam

@Adám maybe add italics to APL386?

Adám

@pVCaecidiosporeadduced that'd be a huge job!

pVC aecidiospore adduced

@Adám how many glyphs does it have?

Adám

@pVCaecidiosporeadduced 892, but many are symbols that wouldn't be affected.

pVC aecidiospore adduced

07:08

@Adám like: ⍺⍵⍒Σ?

and : +-×÷⍝⍀/\⍎⍕;'?

Adám

Yeah.

pVC aecidiospore adduced

07:19

my headphone is annoying

yes it is very annoying

lyxal

that's an odd name for headphones

I just call them headphones

Because I don't go around saying "I listen to music with my very annoyings"

I say "I listen to music with my headphones"

/s

pVC aecidiospore adduced

lol

Bubbler

insert another joking joke here

pVC aecidiospore adduced

JoKing vs joking

windows doesn't recognise a difference

JoKing = joking

windows yes

oh ok

technically all BASIC programs scream

Unrelated String

thanks for linking natural number game
i may have just burned like two hours on just getting to the power level but this is fun

pVC aecidiospore adduced

08:13

how come i write 3 pages but my friend writes 7 pages

hyper-neutrino

08:36

if i have my induction set up as i : n * (a + b) = n * a + n * b, why can't i use rw i, on succ n * (a + b) = succ n * a + succ n * b? (doing the nat num game rn)

is it cuz succ n doesn't "count" as a member of the naturals?

Bubbler

i's left side is the very specific pattern n * (a + b) for already fixed values of n, a, b, so it cannot match anywhere in succ n * (a + b) which is (succ n) * (a + b)

hyper-neutrino

oh, i see... well then i'm stuck cuz i don't have a succ_mul or any commutativity yet and i managed to make a loop by breaking succ down into addition lol

New Posts

0

Q: Lean golf: Balanced Bracket Sequence

A bracket sequence is a string that consists of the characters ( and ). There are two definitions of a balanced bracket sequence. Definition 1 The empty string is balanced. If a string x is balanced, "(" + x + ")" is also balanced. If x and y are two balanced strings, x + y is also balanced. De...

code-golf balanced-string proof-golf lean

Bubbler

I guess I'll need to re-complete the nat game on every device I have, to figure out where the others are :P

hyper-neutrino

i ended up rewriting it from the top and picking another thing to do induction on lmao

Bubbler

08:50

Please come to the Lean chatroom if you have any questions about Lean challenges or the Natural Number game.

6

Yeah, knowing how to pick which variable to induction is one of big skills in theorem proving

pxeger

@RedwolfPrograms just go to space and travel at the speed of light for a few years (or would that make you even younger? I'm no good at relativity)

Bubbler

Time to kill the nat game at the office PC

Adám

@pxeger Yes, faster travelling makes time progress slower, so one ends up lagging behind the rest of the world.

New Posts

09:11

0

Q: i made this thing on a bytebeat composer named dollchan. do you like it? (11025Hz)

(t%200|t%201>>2)|(t>>4^1000|t%202)

code-golf math code-challenge music

hyper-neutrino

what?

pxeger

seems to be a way of generating music using what are essentially hash formulae

but it's just more butter

Bubbler

09:33

... and I just realized that the nat game mysteriously fails to load here

frick

7

pVC aecidiospore adduced

09:49

@NewPosts how much rep do i need to veiw deleted posts

Bubbler

10k

New Posts

10:24

0

Q: Revert Flow Free puzzle

Inspired by Is this Flow Free puzzle trivial? by @Bubbler. Lengthy chunks of this challenge are borrowed from there. This may be one step of a solution for the linked challenge, depending on chosen strategy. Background Flow Free is a series of puzzle games whose objective is to connect all the sa...

code-golf array-manipulation grid

user

11:24

@pxeger No, redwolf should go to the moon and accelerate the earth away from him

Adám

@pVCaecidiosporeadduced Do you know about this list?

Sandbox Posts

12:38

0

A: Sandbox for Proposed Challenges

Give me the border code-golfarray-manipulation Inspired by Is this Flow Free puzzle trivial? by @Bubbler. Lengthy chunks of this challenge are borrowed from there. This may be one step of a solution for the linked challenge, depending on chosen strategy. Challenge Given an array of digits 1-9 and...

caird coinheringaahing

12:55

Just a PSA: please don't vote to delete questions that are closed as "Needs details or clarity", (example), especially if they have answers, as, however unlikely, the OP may come back and attempt to fix the challenge. If these posts really should be deleted, then the automated Roombas will clean them up. Save your VTDs for things that should be removing as quickly as possible (e.g. butter, spam, etc.)

It also doesn't help that deleting these posts undoes the reputation earned by the answers, if done within 60 days of posting :/

lyxal

@NewPosts y'know, I was always wondering why it's called "Flow Free" in the title of both questions, because I was like "why tf you referencing the free version? Isn't the paid version literally just the same puzzle" but then I saw that "free" is quite literally part of the name of the app and that there is no flow paid

This is so sad alexa play despacito

caird coinheringaahing

@lyxal why is it sad that there isn't a paid version?

lyxal

Because I was going to purchase it from the play store to make a joke along the lines of "y'all playing the free version while I'm being a gamer playing the paid version"

And that would have potentially resulted in 4 or 6 stars on the starboard because it would have been a haha funny joke

Now I've got no haha funny joke on the starboard and it's time for bed

Hence why I need alexa to play despacito

caird coinheringaahing

I have to say, I've never considered paying in order to get something on the starboard :P

lyxal

well it's not like it's my money anyway

I would have just used the free play store credits I get from doing google surveys lol

I'm desperate for validation via meaningless stars, but not that desperate to use my own money

caird coinheringaahing

13:02

@lyxal If you're stealing money in order to finance TNB jokes, we may have to have an intervention for you :P

lyxal

@cairdcoinheringaahing why you gotta be a spoilsport like that? Everyone knows that you don't get stars without some sort of illegal funding /s

caird coinheringaahing

Yeah, but stealing is the worst form of illegal funding. Do what the rest of us do and enter into a pact with the God of Code Golf

lyxal

Heck no

Stealing is original

And I'm all about original

caird coinheringaahing

Isn't stealing, almost by definition, not original? :P

Bubbler

If anyone's wondering, I enjoyed all three games in the Flow Free series (vanilla, Hexes, Warps), grinding for all achievements (which include three "play 365 daily puzzles")

(and if you want Flow VIP, just buy all packs + remove ads. I did for all 3, and they're worth it)

Aaroneous Miller

13:11

y'all playing the free version while Bubbler being a gamer playing the paid version

lyxal

@AaroneousMiller mfer really went and stole my joke smh. :p

Anyhow it's bed time for me

Aaroneous Miller

o/

lyxal

ooooooooooooooooooooooooooo/

Aaroneous Miller

o/o

lyxal

(i stole heads tonight because it's funny)

2

Aaroneous Miller

13:15

i only worked on the cop for a couple minutes last night before i got distracted, so imma actually work on it today

pVC aecidiospore adduced

@lyxal /

(my head got stolen by lyxal)

Redwolf Programs

13:35

o/

Oh wait I'm a little late

@cairdcoinheringaahing 16 as of a few weeks ago

@Adám Time to accelerate all of you to the speed of light

Redwolf Programs

13:53

Aaroneous Miller

14:09

Clearly the person on the left is displaying some of the objects he has managed to produce by means of his new 3D printer, and the person on the right is the one who's mind has been addled by the use of Java, thereby preventing him from making the connection between the new printer and the objects displayed before him.

In fact, now that I look more closely, you can tell from the continuous background between the two sides of the image that there are in fact two pairs of people: Person A displaying his printed burrito to Person B, and Person C displaying his printed turtle to Person D. Both of these exchanges are happening simultaneously, meaning that both Person B and Person D have been infected by vile clutches of Java.

Aaroneous Miller

14:23

idea: a lang that is almost entirely builtins for certain functions, but they're all for super specific and complex tasks, such that stringing them together to perform more basic tasks is actually longer.

Huỳnh Trần Khanh

14:35

@AaroneousMiller wow this idea is p neat lol can you implement it

Aaroneous Miller

@HuỳnhTrầnKhanh I want to, but I already have like 5-6 other langs I'm in the process of defining/implementing, so I don't know when I'd be able to get to it.

pVC aecidiospore adduced

CMQ: Glyphs for splitting an object into 2?

like [1,2] -> [1],[2]

pxeger

x?

or | or -

Redwolf Programs

½

pVC aecidiospore adduced

@pxeger ty i will use this

@RedwolfPrograms used as vectorized half

Bubbler

14:49

⍠

Aaroneous Miller

/

pVC aecidiospore adduced

uh ok enough

github.com/PyGamer0/dinoux/blob/rewrite/docs/Elements.md

CMQ: Glyphs for Reciprocal.

Wheat Witch

Isn't there a bot that posts new hello world submissions?

Redwolf Programs

A feed

So it's slow

Wheat Witch

Ah ok.

Redwolf Programs

14:59

@pVCaecidiosporeadduced ⅟ ("Fraction Numerator One")

Or overload ¬

pVC aecidiospore adduced

@RedwolfPrograms that will do

Redwolf Programs

Cover your eyes, this is a vulgar fraction: ½

"Vulgar Fraction One Half" :p

TIL Unicode has a character specifically designated as Euler's constant: ℇ

(U+2107, "Euler constant")

pVC aecidiospore adduced

in Dinoux Room, 31 secs ago, by pVC aecidiospore adduced

Asking feedback for the 69th time: eee

@RedwolfPrograms ℇℇℇℇℇ

:ℇ or ℇ:

Aaroneous Miller

:3

Hello, World!

1

A: "Hello, World!"

قلب repl, 21 bytes قول"Hello, world!" Online repl Qalb is a programming language designed for Arabic speakers as opossed to the anglophone stance of most popular programming languages. I took this program from wikipedia and fiddled around with it, managing to save 3 bytes. If you were wondering...

user

15:29

@RedwolfPrograms wut

@lyxal They’re not meaningless if they help you pretend that people think you’re funny and your views matter

Aaroneous Miller

@user Out of curiosity, would this qualify for your bounty? At the time of posting, there was another answer, though it turns out it wasn't valid, which is why it was deleted.

New Posts

0

Q: Tips for golfing in lean

Lean is a theorem prover and programming language. It's also as of writing the Language of the Month! What tips do people have for golfing in Lean? As always, tips should be specific to to Lean (e.g. "Remove comments" is not an answer), and stick to a single tip per answer.

code-golf tips lean

caird coinheringaahing

16:15

@RedwolfPrograms In case I didn't say it closer to the time, congrats!

pxeger

the eternal struggle

Wheat Witch

I want to implement it.

pxeger

can I send you a repo full of inconsistent specification docs for a language I want implemented, most of which are bad ideas?

Aaroneous Miller

@pxeger Hey, I have one of those too!

pxeger

@AaroneousMiller more like 5...

I present to you, a genuine quote from a compiler I have['nt] written:

def valid(self, compiler_state):
    # TODO: implement type-checking
    return True

Aaroneous Miller

16:26

@pxeger Well, I have a single one for all my languages. So far I have Quest, brainhex, Jumble, Cursed, Plum, and Hello Hell, as well as a small idea I came up with earlier that I have yet to flesh out. :/

Oh, and Parity, though that one's more of a basic concept that I'm not sure if I'll ever do anything with.

pxeger

@AaroneousMiller this is 5 would-be practical languages, esolangs are a whole different story... lol

Aaroneous Miller

ah

yeah mine are all esolangs

well I guess Cursed is kind of in between. It's more of an esoteric praclang

@RedwolfPrograms the More User Details userscript doesn't seem to be working

Redwolf Programs

16:46

Yeah, it broke almost instantly since they changed the layout again

Aaroneous Miller

oh

Redwolf Programs

I'll get annoyed enough to fix it some time in the next few weeks probably

It shouldn't take more than ten minutes

Aaroneous Miller

17:04

Is there a way to tell if something was flagged by a user or was automatically flagged by Community?

hyper-neutrino

yes, just be a mod :p

Aaroneous Miller

sweet, brb

:P

Redwolf Programs

If this is for the LQP queue, usually the community flagged ones have the flag reason as something like "too short" or "too much code"

Aaroneous Miller

yeah, that's what I was wondering about

I didn't know if someone had flagged it or smth for violating the default I/O or if it was just Community being Community

hyper-neutrino

was it this post?

Aaroneous Miller

17:12

ye

hyper-neutrino

yeah that was never flagged

Aaroneous Miller

o

Aaroneous Miller

17:38

@RedwolfPrograms when plumber rewrite?

Redwolf Programs

Not sure. It's very scary to implement, and I think there's a lot of UB

Aaroneous Miller

UB?

Redwolf Programs

Undefined Behavior

Aaroneous Miller

ah

Redwolf Programs

I think I've developed a KotH in a whole new way from my usual method

Aaroneous Miller

17:43

I came up with a notation for plumber that would have each command as 1 character, and then I got an idea for a language using that where the commands could do different things based on the number of packets that were pushed into them, and from what directions. It's kind of like a superset of plumber, with golfier notation.

Redwolf Programs

I wrote what's basically a controller just for fun, and then realized it'd be fun as a KotH

Aaroneous Miller

lol

@AaroneousMiller I'm thinking about calling it Plum, and I think it would be neat to implement.

Redwolf Programs

Sounds like a cool language

Aaroneous Miller

Here's a little example of it: gist.github.com/AMiller42/a623d03e5ae3e2ac9cc7cf0250b37a53

I also wrote a little script to convert Plumber to Plum, or Plum to Plumber: gist.github.com/AMiller42/a39d903b0e38c78385566750367058ff

I was thinking about making an interpreter in Python that would be able to interpret either one, but I never got around to actually doing it.

Redwolf Programs

That sounds pretty cool

I halfway regret not making plumber use single characters since it'd be easier to read

But idk, there's a few advantages to this method I guess

Aaroneous Miller

17:54

yeah, i think it's pretty neat

I actually find it easier to read than Plum, but I created the notation with the intent of being golfier, so ¯\_(ツ)_/¯

hyper-neutrino

19:12

so we're starting formal deduction in my cs245 class, and the format is extremely similar to the natural number game so this is a very convenient coincidence

~~now i can say i'm being productive when i waste time playing the game~~

Redwolf Programs

19:29

I just came across a very interesting way to organize desktop shortcuts

Aaroneous Miller

oh?

Redwolf Programs

One of the teachers in a classroom I walked by had their desktop background image thingy set to a grid of squares labeled "work", "trash", "shortcuts", etc.

And they just dragged them somewhere within that box

And there were some things in between the boxes, which were presumably both "trash" and "work" or similar

Nothing aligned to grids or anything, just randomly scattered

Aaroneous Miller

one of my classmates did something kind of like that, except instead of boxes, he just used a stock image of an office and put icons where they would make sense: text files went on the corkboard, shortcuts went on the desk, the recycle bin was on the floor next to the desk, etc.

Redwolf Programs

lol

I only lol here because as soon as I stop I will D:

Aaroneous Miller

lol

Redwolf Programs

19:34

Oh nice, my login credentials for the Canvas account I was assigned for Latin have stopped working

Aaroneous Miller

\o/

Redwolf Programs

Even better, the forgot password button leads you in an endless circle

Aaroneous Miller

google.com/…

I've trained google well. If I just type y into the search box, it autocompletes to youtu.be/dQw4w9WgXcQ

Redwolf Programs

student login -> forgot password -> a different login page -> forgot password -> "your email is not in this system. try student login" -> student login

Aaroneous Miller

I thought you liked recursion?

Redwolf Programs

19:39

It's not recursion if I do it with jumps :p

Aaroneous Miller

true

Redwolf Programs

Oh...y'wanna know why it wasn't working?

If you go to their homepage it redirects to login, and if you try to login when you're already logged in it gets sad

Turns out I should've gone to a completely different domain that redirects to the correct ones but only when there's a full moon and you say magical words first

Aaroneous Miller

Wait until a blue moon, just to be safe

> I'm an optimist mostly because no country has attacked another with a nuclear weapon since 1945 and because it takes fewer clicks to clean Wikipedia than to vandalize it.

Two great reasons for optimism right there

Redwolf Programs

I'm an optimist because PHP is declining in usage. When the last PHP users steps back from their computer, realizes what they've done, and jumps off their roof, world peace will be achieved.

Aaroneous Miller

Whelp, time to learn PHP!

Redwolf Programs

19:48

Don't do it! You (might, idk) have a family! You have so much to live for!

Step away from the keyboard, there's plenty of support for people considering PHP.

Aaroneous Miller

I mean, I already learned JS. I might as well go all the way, right?

Redwolf Programs

JS is nothing compared to PHP.

Aaroneous Miller

But think of all the destruction I could wreak with such knowledge!

Redwolf Programs

JS has some mistakes and flaws which make it fun to make fun of, but PHP will wait until you're not looking, salt your crops, kill your family, burn down your house, and throw rocks at your cat.

Aaroneous Miller

So what you're saying is, if I learn PHP, it'll give me an awesome superhero backstory?

Redwolf Programs

19:52

No, because it'll corrupt you. It won't do those things on its own, it'll make you do it.

And then you go into town to SQL's house, look through the window at him holding a knife and grinning, and decide he seems friendly.

Aaroneous Miller

in Vyxal, 4 hours ago, by Aaroneous Miller

Oh yeah, I forgot. I don't actually know SQL.

Redwolf Programs

lītigiōsus...when the latin is sus 😳

DLosc

20:24

@RedwolfPrograms On the contrary! Recursion that uses jumps is the best kind of recursion.

Redwolf Programs

Hmm, at that point is it considered recursion though, or just something functionally equivalent?

You could write the typical recursive factorial implementation using a for loop and a variable for state, and that could theoretically compile to the same thing

3

Aaroneous Miller

20:44

that moment when you realize that Vim won

DLosc

@RedwolfPrograms Is that similar to butt dialing?

Redwolf Programs

I can't believe nobody's managed to outgolf the current shortest Hello, World! program in so long

Unrelated String

21:03

@RedwolfPrograms i feel like it probably usually does

actually maybe not because that's not actual tail recursion

but a smart enough compiler can probably figure it out

DLosc

> This article may require cleanup to meet Wikipedia's quality standards. The specific problem is: SOMEONE FIX THE HEADINGS OR THE CONTENT SO THEY ARE MUTUALLY CONGRUENT. Please help improve this article if you can.

Whoever added that notice was not having a good day. :P

@RedwolfPrograms You could also write any recursive function using a loop and a stack. I suspect recursion has more to do with the way the algorithm is written than with how the compiler implements it.

user

21:23

@AaroneousMiller Absolutely! Add your answer and I'll give you 400 rep when I can

@UnrelatedString Wait, can't you write factorial using tail recursion?

hyper-neutrino

you can yeah

Hello, World!

0

A: "Hello, World!"

Vim, 14 bytes iHello, World! Try it online!

user

@pxeger On the contrary, everyone wants to implement them afaict, but only very few succeed, and even fewer get their languages to be popular

hyper-neutrino

f(x, a = 1) := a if x == 1 else f(x - 1, a * x)

user

Which language is that? Looks interesting

Some weird variant of Python?

hyper-neutrino

21:27

pseudocode

DLosc

@user Try it online!

There's also a factorial function in the standard library which is defined as (lambda (num) (product (1to num))), offloading the work to other tail-recursive functions

Sandbox Posts

0

A: Sandbox for Proposed Challenges

Create a program in lang A that prints a quine in lang B Please lmk if this already exists idk how to format this fancy-like which is why im in the sandbox about it I'm also unsure about scoring; I'd like you to be scored on how much shorter program A is than program B but I also want both quines...

user

Reminds me of that thing where different kinds of programmers write the factorial function in Haskell in different ways, and at the end the experienced programmer just does something like fact n = product [1..n]

hyper-neutrino

well at least they know about the sandbox

rak1507

the real experienced programmer does fact = product . enumFromTo 1

hyper-neutrino

21:40

this seems like an uninteresting extension of both just "make a quine" and "print a string"

user

@rak1507 Wait, is that omre idiomatic? Seems less readable to me

rak1507

lol idk just pointfreeing bc why not

user

Why not? Because it's pointless

hyper-neutrino

i love how pointfree uses .

although here there are actually fewer points cuz of the .. in the first one

rak1507

lol

user

21:42

@hyper-neutrino ⍤

Unrelated String

@user i assume the "typical recursive factorial implementation" is the one that doesn't though

user

True, it's easier to write it without that

Unrelated String

and specifically i think the non-tail recursive factorial is a fairly standard way of introducing recursion to people

user

21:58

lol, we were taught recursion by being shown a loop that printed * five times and then being shown the recursive version

Unrelated String

lol

user

I thought it was the most useless thing in the world

Transcript for