1. 2

    I want to understand this, but I need to start with the motivation.

    Why would I be interested in corecursion and coinduction? What does it get me? When might I use these things?

    1. 1

      Whenever you have a computation that works on a stream then you have a co-inductive structure at hand. A web server receiving requests and serving responses all day is quite different from a compiler because one works on a stream of data while the other works on files it can read fully (and will not work otherwise). The co-inductive part also comes with its own problems, co-recursion must be proved productive (it will return a response and a new stream) to advance the stream decomposition and return data to the client. Proving productivity syntactically does not always work and you have to come up with some alternatives (e.g. sized types) but you also have to come up with a sound way to decompose a stream, usually done with proving two streams S and (stream-cons a S') are equal up to something, usually a bisimulation.

    1. 2

      Python is already almost pseudocode though… :P

      1. 1

        But we don’t want it to be executable!

      1. 1

        I might be biased but if your dependencies are already packaged then a package would be what you need. Installing a package not only install the software and its dependencies but it also can put configuration in place and you can save custom values in a database like dpkg to generate your configuration from templates. Also dpkg has a curses interface so you can put a lot of information to guide people who are not tech savy.

        For anything fancier than put this file in this directory I would provide a web-ui where your admin can click things and save it to the database/config.

        1. 4

          I expected this <opt-in-script> tag to be defined as a custom element but it’s just ignored by the browser and rendered as a p while there is some JS to turn it into a <script> tag on the button click. It’s actually a quite nice implementation that can be used for older browsers.

          1. 2

            Yeah. No need for anything fancy, the script is less than 500 bytes. IIRC unregistered custom tags used to cause issues in IE8. After that they’ve been handled as unstyled inline elements.

          1. 1

            On Wednesday I have a presentation for my Topological Data Analysis course, it’s coming together but it’s slow. I also want to implement and replicate results from a paper in python+numpy seeing how a common combination is for scientific computing.

            1. 5

              I keep looking a Racket Stories from time to time and I think it’s a good tool for keeping up with development of Racket. You can find both blog posts, packages and papers eventually make their way there.

              1. 1

                The link redirects to the CS dept home page. The article is here in the ACM digital library, which currently doesn’t have any subscriber restrictions or paywall.

                I find it interesting that a paper from 2003 listing canonical reading in computer science has nothing later than 1981. Were there no subsequent paradigm shifts or big advances in the field? I would’ve thought that human-computer interaction, parallel algorithms, and cybersecurity (if that’s within scope) all moved on dramatically in the intervening time.

                1. 2

                  Unfortunately, the author of this paper passed away in 2019.

                  I would hope this paper continuous to influence computer science programs in various education venues.

                  I think, to a degree, the intent of the author was to separate ‘application’ of CS vs ‘foundations’ of CS.

                  Which is why there is a focus on fundamental ways to carry out a ‘compute’.

                  Have there been advances in the foundations of CS since ’81? I am sure.

                  But I could not come up with something that changed a fundamental carrying out of compute (with exception of quantum computing).

                  I think there are multiple new subfields developed, though, with most foundational one being program verification (that extends to verifiable correctness, security, computability limits). I think this subfield will have tremendous long lasting impact for next 100 years. As we will transition of how we teach CS from ‘guessing’ how to build ‘what will work’, to proving that it will work.

                  1. 2

                    The link redirects to the CS dept home page. The article is here in the ACM digital library, which currently doesn’t have any subscriber restrictions or paywall.

                    Thank you! I made an opsie again.

                    I find it interesting that a paper from 2003 listing canonical reading in computer science has nothing later than 1981.

                    They actually address this in the paper, mistery solved!

                    Another aspect of the readings shown is their age: for the most part, we have hewed to a rule that Canon papers should be at least 20 years old to be included in the course. The purpose of this rather arbitrary cut-off point is to provide a rough means of ensuring the lasting interest of the work in question.

                    1. 1

                      Oh, thanks, I didn’t spot that paragraph in the article when I read it. It’d be interesting to consider what writing from 1981-2000 would be included in a modern update of that article using the same rules, but also what the likely candidates are from this millennium too.

                  1. 1

                    Asking as someone with basically no mobile dev experience but with interest in development a mobile PWA (progressive web app), how useful does GeckoView seem for that? Or does it make more sense to focus exclusively on a PWA for the foreseeable future?

                    This would be an authoring app where data preservation and state preservation would be paramount.)

                    1. 3

                      We made a PWA for one of our mobile games and then wrapped it in a native app package with Cordova (because most mobile users are used to downloading apps).

                      On iOS, using the WebView was fine. On Android, it was a giant pain, as several things don’t quite work in WebViews as they do in Chrome. Not to mention the version differences. There are several bugs, annoyances, and inaccurate or incomplete docs related to Android WebView and related APIs (for example, not being able to intercept the body of POST requests). Our PWA worked seamlessly in the mobile browser, but we ended up having to make several changes to make it work in the WebView.

                      Super glad to see this posted today. It might save us from further hackery.

                      1. 1

                        Thanks! I don’t recall hearding about Cordova before and that looks helpful. Particularly grateful for the heads-up on your Android experience because that would be my primary target.

                      2. 1

                        This is an interesting question, I’m not sure which API are exposed to JS running in a webview. Having a full fledged browser embedded in your app can be a boon for modern API that are not available otherwise. I think workers might not be available in a common webview so a PWA re-packaged as an app might have some difficult times. You would have easier life on bundling your assets in the app but all the networking would be quite different, e.g. services workers might be gone.

                        1. 1

                          Thanks for the heads up!

                      1. 2

                        So, why is this coding stream upvoted and mine was marked as spam?

                        Is it because I had posted my own stream? Because I was fixing bugs on an existing project that isn’t particularly popular? Because it was in progress rather than an old stream?

                        I’m just trying to understand what is considered on-topic and what is considered spam. Is it more appropriate to post upcoming livestreams on IRC?

                        1. 8

                          You got one person marking it as spam. This isn’t necessarily indicative of everyone’s feelings here!

                          Personally, I think that this board is maybe a bit not ideal for announcements on time sensitive things, but posting full recordings later if it’s an interesting stream is good.

                          If you are interested in announcing in-progress streams, perhaps the IRC channel would be a better fit? I would click on it if it were posted in there

                          To be crystal clear: I think a lot of people in the community like this kind of content! I imagine the spam vote was from somebody in a bad mood who read your post as “self promotion” (personally doesn’t make much sense to me)

                          1. 5

                            I appreciate that, I’ll try the IRC the next time I stream. Thanks!

                          2. 4

                            This is actually a good discussion that needs to happen here. There are already platforms that do some aggregation of live coding and my opinion is that they work better than lobsters for that. The front page is changing very fast already and having time constrained elements would make it change even faster.

                            1. 2

                              Thanks for the link! I’ll be sure to use that site next time.

                              Edit: This bit does resonate with me;

                              The front page is changing very fast already and having time constrained elements would make it change even faster.

                              I wasn’t planning on posting every stream here, but this makes a lot of sense and I probably won’t post another here unless it’s much more relevant.

                            2. 3

                              Andrew Kelley is definitely a favorite on this site, which makes anything posted immediately more visible. I’m not sure why yours was flagged spam, but perhaps someone didn’t want to see it and needed a reason to downvote.

                              1. 0

                                Ah, so this is just a classic double-standard. Nice.

                                I can understand if nobody liked my stream, but if livestreams are welcome then a “spam” downvote is just false.

                              2. 3

                                This is probably more about what is shown here: The demonstration aspect of what you can do in zig. And about showing people how you can do this live, thus in a reasonable amount of time and effort. This more a show-off how capable zig is already, and lobster is pretty interested in zig and new languages like this. At least this is why I felt like this belongs here, even though I haven’t watched it.

                              1. 3

                                I’ll definitely watch this later when all my meetings are done

                                1. 2

                                  I am working on a C++ firmware where many things can and should be initialized statically so that we can get nice things such as the linker script scolding you for exceeding the RAM available. One of the pattern that makes us all barf is the singleton class, we could add it to the docs but then I would forget and cry. To solve this issue I found about GCC plugins and eventually thought of creating one that when adding a pragma or similar would yell at me when creating the same object twice. I still haven’t done it because the documentation is quite poor for people that don’t dabble in looking inside GCC.

                                  Still I have found so many projects trying to get people going

                                  1. 5

                                    Also worthy of note is Coq in a hurry where it goes on a little more about proofs on inductive proof principles by using the naturals and lists as examples. I used it when preparing my “Type theory and Coq” exam and things were rather pleasant after that except for some nasty functions which I couldn’t get to typecheck and I had to resort to Program Fixpoint to delay some proofs.

                                    1. 1

                                      I really wanted this to be from Ordinary differential equations to J but this is also ok

                                      1. 2

                                        After reading this I couldn’t resist solving the harmonic oscillator numerically in q…
                                        (last line is just ASCII plotting)

                                        q)a:2 2#1 0 0 1+0.01*0 1 -1 0
                                        q)z:2000(a$)\1.0 0
                                        q)" *"[(3-til 7)=\:"j"$3*z[25*til 50;0]]
                                        "***                    *****                    **"
                                        "   **                **     **                **  "
                                        "     *              *         *              *    "
                                        "      *            *           **           *     "
                                        "       **        **              *         *      "
                                        "         **     *                 **     **       "
                                        "           *****                    *****         "
                                        
                                        1. 1

                                          No, this is ok. ;)

                                          EDIT: actually, do you have a link to From Ordinary Differential Equations to J?

                                          1. 2

                                            From Ordinary Differential Equations to J

                                            Unfortunately I haven’t found this yet. Might have to learn me some APL and write it myself.

                                            1. 4

                                              Oh. I get it. “Ode” as an acronym. In my defense I hadn’t had any coffee yet.

                                              If you’re interested in that sort of thing, you might like this: http://www.softwarepreservation.org/projects/apl/Books/CollegeMathematicswithAPL/view

                                        1. 2

                                          Is it JMAP conpatible or it’s just ad-hoc serialization of email and mailboxes?

                                          1. 1

                                            This is an interesting idea. I was not aware of JMAP - thanks. Currently, the code is just finding the “To”, “From”, and “Subject” lines, and adds the the raw mail data with all the fields as received by the SMTP. The whole email “parser” is here: https://github.com/ptek/api.unverified.email/blob/112a1f002bc7bf22651603523de414452be89612/src/Model/Email.hs#L19-L30

                                            EDIT: Is there any particular application you have in mind with JMAP? Dies it somehow help with testing?

                                            1. 5

                                              Compared to IMAP, JMAP is a much simpler spec that more closely matches how people typically use email.

                                              Also, using https as the transport means you get a very widely understood / supported TLS stack vs the compatibility mess that is StartTLS et al.

                                          1. 1

                                            Cool project!

                                            Edit: I’m a bit new to lobsters: Shouldn’t this post have the “show” tag? Just trying to understand this community better.

                                            1. 1

                                              That is probably true. I have not thought of it.

                                              1. 1

                                                When this happens you can also suggest tags!

                                                1. 1

                                                  I don’t think I can do this (I have limited access to stuff since I’m new)

                                              1. 2

                                                I am finally not overloading my watch with interrupts from the accelerometer so maybe some more work on that to be able to tap and interact, I realize now I love application notes. I also have an assignment coming up so that requires more attention.

                                                1. 1

                                                  I use systemd-nspawn a lot for the same purpose, spawn a process in its own namespace from a directory and use it to build something, add different root filesystem or networks as you need and eventually if I really need it add it as a service.

                                                  1. 3

                                                    When I looked into it the label tag was also used to extend the “clicky” target for an input. So if you ever had problems clicking a checkbox on a form you could wrap it into a label and style the label to be used as a larger target. This also means that the two variation (label wrapping an input and label referring to an input) can be positioned differently on your page because of how you are constructing your tree.

                                                    1. 1

                                                      Optimize with Confidence. Using post-conditions, CrossHair ensures that optimized code continues to behave like equivalent naive code:

                                                      This is very interesting but it may be out of reach for an automated theorem prover right? What are the limits when this can be used? I see lists are supported so I guess the builtins are covered

                                                      1. 1

                                                        There are a lot of limits. Some of those limits will get better with time and effort; others will never get better. I’ll try to quickly go through them:

                                                        • Proving arbitrary properties of programs is known to be an undecidable problem. (no matter what, there will be some programs with bugs that CrossHair can’t detect)
                                                        • CrossHair uses the theorem prover only in the context of a single path of execution. Most interesting functions have an infinite number of paths: CrossHair can only verify a finite number of them. The Fuzzing Book that @vrtha mentions above actually has a wonderful description of how this works.
                                                        • Yes, most of the builtins (lists, dictionaries, sets, etc) should work, but I have to say that the way we implement this is pretty delicate, and I need people to use it in order to find the cases that don’t work properly. (please help me! 😁)
                                                        • As for the standard library and 3rd party modules, pure python implementations should work (since they can use the symbolic builtins), but modules implemented in C will generally not be analyzable. To fix this, we can sometimes re-implement such modules in pure Python and tell CrossHair to use those implementations instead.
                                                      1. 2

                                                        “Programming” also covers the programming environnent or does not? A full blown unix programming environment article might be “practices” but a (build) tool alone still fits in the “programming” umbrella which is by default quite large

                                                        1. 5

                                                          Maybe I just hate the programming tag because it’s so general.