1. 4

    Some time ago I learnt this

    import this as love
    love is True
    love is False
    love is love
    

    despite being silly it shows that Python has modules and you can manipulate them!

    1. 2

      Another thing I just found :)

      import this as love
      print(''.join([love.d.get(i, ' ') for i in love.s if i]))
      
    1. 15

      I will learn:

      • More number theory and error analysis so that I can implement the Elusive Eight.
      • More about BATMAN and mesh networking, so that I can keep improving my home network.
      • More about implementation of databases so that I can implement a proper categorical database system.
      • More about Z3’s internals. I think that I have an improvement on the state of the art for 3-SAT but I’m not sure yet because I haven’t grokked every internal representation of Z3.
      • To get better at proposing simple natural arguments which infuriate bigots, so that I can more effectively create self-doubt and insecurity amongst fascists.
      • One additional algorithm for a non-standard Rubik’s Cube. Probably parity fixes for 4x4/5x5 or last-layer for Megaminx.
      • To keep Venus flytraps alive. Surprisingly picky plants, and I don’t have a green thumb.
      1. 4
        • More about implementation of databases so that I can implement a proper categorical database system.

        Can you tell me more about “categorical database system”? I stumbled upon http://math.mit.edu/~dspivak/informatics/talks/CTDBIntroductoryTalk it looks interesting. Thanks!

        1. 5

          Imagine a database that is not built on relational logic, but on categorical logic. Imagine not just graph databases, but databases which store hypergraphs with path equivalence; that is, databases in which categories are the objects being searched and stored.

          Alternatively, imagine a language for expressing categorical ideas. I keep coming back to Hagino CPL, a language in which one writes lengthy categorical expressions, and retrieves a canonicalized shortened categorical expression.

        2. 2

          More about BATMAN and mesh networking, so that I can keep improving my home network.

          Are you using mesh network at home? Which devices are you using for it? Is there a real advantage using a mesh network at home instead that using a traditional network?

          1. 2

            More about Z3’s internals.

            Z3?

            1. 7

              The Z3 Theorem Prover, an efficient SMT (Satisfiability Modulo Theories) solver very popular and widely used in Formal Methods and PLT (Programming Language Theory) research communities.

              Programming Z3 is a nice tutorial with references to other great resources about Z3.

              1. 11

                A roadster built by BMW in the 90’s and early 2000’s. I also have a somewhat broken one that I need to learn more about it’s internals to get it roadworthy again.

                1. 1

                  A SMT/SAT solver by Microsoft

                2. 1

                  3-SAT is, as far as I can tell, mostly a theoretical device. SAT solver implementations deal with arbitrary clauses (but have special optimizations for 2- and sometimes 3- clauses). I’d recommend looking at minisat/glucose/cadical rather than Z3 if you’re into pure SAT because Z3 is a SMT solver and is literally orders of magnitudes more complex than a SAT solver.

                  1. 1

                    To keep Venus flytraps alive. Surprisingly picky plants, and I don’t have a green thumb.

                    I was endlessly fascinated by these as a young man and killed a great succession of them, probably due to over-feeding.

                    1. 1

                      To get better at proposing simple natural arguments which infuriate bigots, so that I can more effectively create self-doubt and insecurity amongst fascists.

                      This is something I’ve been thinking about for a while as well. Do you think they are open to the voice of reason/argument?

                    1. 2

                      It’s been a trend for some time, Python has been taking over the introduction to CS courses because it makes some nice compromise that actually help when learning. I liked it a lot but I currently loathe it a little seeing some resources available to LISPers, I liked “the little schemer” a little too much and it beats any Python introduction I have been given by far.

                      1. 1

                        I have recently began writing bucklescript bindings to the webextension API and I’m happy to report that it was a very nice experience with two gotchas. First the JS module system is not available to the extension runtime in FF except if you load your scripts from a background page (go figure) and second a lazily evaluated language can have some problem modelling the functions you receive from the browser. Even if you have a function type A * B => C which checks out the runtime might desugar this to A =>B =>C and do partial applications. The nice part is that Ocaml has an escape hatch to make uncurryed functions so it was relatively easy to fix.

                        1. 2

                          It’s interesting to see how reviled Ada was at the time. Nowadays, there seems to be a rehabilitation of it, especially in the wake of Rust.

                          1. 1

                            Nowadays, there seems to be a rehabilitation of it, especially in the wake of Rust.

                            I’ve seen maybe one blog post recently talking about Ada. Have I just not been looking in the right spots?

                            1. 1

                              Some things I remember from last year, I guess they were not posted on lobster

                              1. 1

                                I mentioned it sometimes here: the Ada folk are regularly quite happy about Rust, because it opens up the discussion again. And with SPARK and other things, they have quite to products at the ready.

                            1. 2

                              Not something like this but openwisp is a tool that I worked on that gives you a pretty interface to specify the configuration for network devices. You have a daemon reporting the hash of local config to the server and eventually it downloads the one from the db if the hash is different.

                              This way you keep the config in the server and the device just overwrites local changes. It’s used mainly to administer fleets of devices, e.g. an eduroam clone.

                              1. 5

                                I like this peek behind the curtains but the most important piece of information in there for puzzle/contest designer is to make sure you can just ask for the one output, not a whole program (looking at you ICFP!).

                                Every time I had to submit code for some contest it was definitely a dreadful experience, having to send just a solution was always nice.

                                1. 1

                                  I am so done with the Nordic soft device; next I am looking at mynewt-nimble to get bluetooth working and having traditional Goan food tonight

                                  1. 3

                                    strace + man can yield very good building blocks. I am mostly curious about one nitpicky thing so this might be the fastest route. After googling the hell out of it.

                                    1. 1

                                      I’m a long time user of OpenOCD, but lately I’ve been getting more excited about ARM’s PyOCD project. It’s a very well structured piece of code, written in Python. It’s very easy to extend, though it doesn’t support quite as much hardware as OpenOCD. https://github.com/mbedmicro/pyOCD

                                      1. 1

                                        This is very interesting, I really like the Micro:bit use of CMSIS-DAP, it has two chips on board, one is the programmer and USB mass storage! You can flash by literally drag & drop mindblown.

                                        It looks like I will soon need a new adapter to try this out, unfortunately mine are not supported.

                                      1. 1

                                        Are they selling the dev kits?

                                        1. 1

                                          No, you had to ask nicely in September when they announced the dev kits.

                                          1. 1

                                            Yeah, I think then I was realistic that I wouldn’t actually have the time to do something cool with it :)

                                        1. 5

                                          I bought a used ThinkPad x230t off eBay a few weeks ago, and I’ve been using it to mess around with non-server Linux for the first time in ~15 years. I just got the tools to coreboot it, so I’ll be doing that this weekend, depending on time.

                                          1. 3

                                            Go to the coreboot irc because sometimes the wiki is not truly updated and articles about flashing coreboot are not the best source of information. I fried mine 2 years ago, had to make a run for another motherboard, not fun. Do not connect VCC to the clip, have the chip draw current from the internal bios battery and make sure to enable wake on lan so that sticking a LAN cable actuallly powers up things in the board controller. I actually wrote some more about my problem, take care.

                                            1. 1

                                              Thanks for the advice! I powered it through Wake on LAN, and it seems to have gone smoothly. The only weird thing I’ve noticed is that grub only takes up the top-left corner of the screen, but that’s totally fine. Flashed it again with the extracted VGA blob, that fixed it.

                                              1. 1

                                                make sure to enable wake on lan so that sticking a LAN cable actuallly powers up things in the board controller

                                                This is really great advice, and something that took me a while to find a couple of years ago when I put coreboot on mine. The option to enable WOL is in the lenovo bios that you are about to replace, so don’t forget to enable it before you try to flash!

                                              2. 2

                                                Welcome to the club. I’ve been using Linux as the exclusive OS for my laptops and desktops for around 15 years now. Linux is more than ready and capable for regular daily usage, possibly excepting the most specific of power user applications.

                                                1. 1

                                                  Yeah, I’m impressed. Everything seems to work out of the box, and I’ve been finding good cross-platform replacements for the software I’d been using.

                                                2. 2

                                                  Sweet! Couldn’t have more positive things to say about my X280 - such a wonderful machine. I had used a MacBook Air 11” (running nixos) before making the complete switch.

                                                  1. 1

                                                    Nice! I switched to nixpkgs on Mac a year or so ago after being unhappy with the direction Homebrew was going. Wanted to try dual-booting, but it seems like no MacBook made in the past few years can run Linux well anymore. The last time I tried, the keyboard wouldn’t even work on the livecd boot screen.

                                                    Finding a decent machine for <$100 was mindblowing and seemed like a good way to get started. So far, it’s been even better than I expected!

                                                1. 2
                                                  define check_relation
                                                   psql -d $(PG_DB) -c "\d $@" > /dev/null/ 2>&1 ||
                                                  enddef
                                                  
                                                  check_relation "damn_table"
                                                  

                                                  Is it just me, or is this not even close to actual functioning code?

                                                  For one thing the relevant keyword is endef (one d, not two); for another, that’s…not at all how function calls look in (g)make. For a third, calling that definition a “function” seems like a bit of a stretch, since it’s not parameterized (no $1 references or anything).

                                                  1. 2

                                                    Thank you for the feedback, I’ve included the whole example from DataMade so it would be more clear how this fits. Basically it does substitute the value of the command to the check_relation it finds in the text so I would call it a function but it is true that it should not be parameterized.

                                                  1. 2

                                                    I had no idea GNU Make is extensible with Guile. That’s the most important takeaway I got from a silly post lately.

                                                    1. 2

                                                      I had no idea make was extensible at all, hence the post!

                                                    1. 1

                                                      I’m wondering if this is the standard way to put dependent types in Haskell, stuff like nonZero and nonEmpty are the bread an butter of this patterns. Also he bashes the Option type to then use it instead of providing the proof.

                                                      In coq I would use the exist constructor to construct the return value of the function so that you can encode both the return value, the return type, the predicate the value satisfies and the proof of the return value being a witness.

                                                      1. 1

                                                        exist works—it reduces the size of the range to only those values for which a compatible witness exists.

                                                        This kind of stuff can be done to some degree with Liquid Haskell, but it’s far from mainstream.

                                                        You can also do some amount of Coq-like dependent typed technique in Haskell if you’re willing to pay the tax of a much less expressive language.

                                                      1. 8

                                                        Thanks to the Clawlateral committee for running this fancy part of the internet!

                                                        1. 3

                                                          V.v.V

                                                          1. 2

                                                            🤘.V.🤘

                                                            1. 1

                                                              (/) II (/)

                                                          1. 1

                                                            The claims in this paper would not get past the advertising standards authority.

                                                            The usual development process was followed, i.e., specification, implementation, compilation.

                                                            Then some theorems were stated. Voila, the code is verified.

                                                            As always with formal methods snake oil, the term correctness keeps popping up. They even have a “single end-to-end correctness theorem”.

                                                            1. 2

                                                              I don’t understand your skepticism about CakeML and and correctness. From what I heard and can read around it’s a compiler that has verified passes in the sense that they proved theorems about the behavior that can happen in every one of them. In the end you can combine all you proofs about the little passes in a bigger proof for you compiler and prove your compiler correct up to the specification introduced by the theorems.

                                                              1. 2

                                                                What does it mean to prove a theorem about some code?

                                                                You might prove,say, that some algorithm never exceeds some limit; and the code is an implementation of that algorithm. So, modulo bugs in the code, it will never exceed the limit proved.

                                                                This does not prove the code is correct, only that the limit is not exceeded.

                                                                What can be said about a sequence of chunks of code, each associated with an algorithm that has an associated proof of some property? Individually they have the proven properties, but as a whole? What of emergent behavior?

                                                                1. 1

                                                                  This argument can be used to attack pretty much any security guarantee provided by everything from cryptography to access control to formal proofs. You’re not really saying anything here and you’re certainly not actually digging into the proof to point out gaps in their logic. Its a value free over-generalization that adds nothing to the conversation. Flaws in methodology, even formal methods methodology, do not automatically make a method “snake oil” as your original post put it.

                                                                2. 1

                                                                  He did eventually tell me what he thought about that. Lobsters search isn’t giving me the exact comment, though. He’s an empiricist that wants to see theories confirmed with experimental data. Most paper on formal verification do proof but no testing or even peer review. Write-up’s like Guttman’s showed some historical programs with proofs failed on one execution or inspection. My current guess is that he’d prefer each of these theorems to have a good number of experiments and review showing that they work. Then something similar for each integration with or layer on top of them.

                                                                  An example of some validation of verified program was Csmith testing of multiple compilers, including CompCert. The testing found piles of errors in other compilers but only 2 or 3 in CompCert’s specs (not just code). This offered, for such inputs, evidence that CompCert’s methods had high quality, may be better than others (apples to oranges comparison), and code didn’t add additional errors on top of spec [1].

                                                                  Although a fan of verification research, I support the position I just described. A mix of methods was the default for high-assurance security and other reliability/security-focused projects in the past. Here’s an example (pdf) showing why: different methods catch different problems. It’s the assurance version of defense in depth. In another example, the seL4 team put all their eggs in the formal verification basket. Whereas, INTEGRITY-178B had to do a lot more to get certified at EAL6+ High Robustness. The requirements, listed in bottom right boxes, included a mix of formal methods, thorough testing, leak prevention/analysis, and independent pentesting. My own requirements for high-assurance are a superset of what they did.

                                                                  [1] @derek-jones, am I properly qualifying that?

                                                                  1. 1

                                                                    My response has nothing to do with experimental proof.

                                                                    The claims being made (e.g., correctness) are not justified by the theory work that has been done.

                                                                    1. 1

                                                                      Oh OK. I can’t evaluate that since I can’t read their specs and theorems. If I validated it, I was going to recruit one of them to just tell me what each means so I could write test generators and checkers for them. Manly was interested in WordLang and DataLang as verified backends for non-ML compilers.

                                                              1. 4

                                                                I thought codata was related to corecursion, in fact serving a similar purpose to Python generators. My notion of codata comes from the Idris construct of that name:

                                                                codata Stream : Type -> Type where
                                                                  (::) : (e : a) -> Stream a -> Stream a
                                                                

                                                                This gets translated into the following by the compiler.

                                                                data Stream : Type -> Type where
                                                                  (::) : (e : a) -> Inf (Stream a) -> Stream a
                                                                

                                                                This is similar to what Wikipedia has to say:

                                                                Coinductively defined types are known as codata and are typically infinite data structures, such as streams.

                                                                Are these two separate notions with the same name or am I missing a connection here? Granted I kind of skimmed both texts.

                                                                1. 3

                                                                  codata is indeed related to corecursion. Let’s say you have a functor F and let’s look at two things in category theory. F maps the object X to F(X) and by inversion of the arrow we also have the mapping F(X) -> X.

                                                                  Let’s look at a simple functor like F_A(X) = 1 + A x X. It defines the algebra for lists over A when we consider F_A(List_A) -> List_A, we either have an empty list (nil or 1 in the notation) or pair of an element and a list that we can cons, these are called the constructors and we use them for data. The other direction of the arrow is X -> F_A(X)and defines the stream over A with termination StreamT -> 1 + A x StreamT. In this direction we observe the stream ending (1) or we get the head and tail (A x StreamT), the cocostructors are used to observe the stream and indeed they are codata. The idea is that data and codata are the two directions of the functor relation!

                                                                  1. 1

                                                                    Great, now it makes more sense, thanks

                                                                  2. 1

                                                                    The paper abstract:

                                                                    Computer scientists are well-versed in dealing with data structures. The same cannot be said about their dual: codata. Even though codata is pervasive in category theory, universal algebra, and logic, the use of codata for programming has been mainly relegated to representing infinite objects and processes. Our goal is to demonstrate the benefits of codata as a general-purpose programming abstraction independent of any specific language: eager or lazy, statically or dynamically typed, and functional or object-oriented. While codata is not featured in many programming languages today, we show how codata can be easily adopted and implemented by offering simple inter- compilation techniques between data and codata. We believe codata is a common ground between the functional and object-oriented paradigms; ultimately, we hope to utilize the Curry-Howard isomorphism to further bridge the gap.

                                                                    Emphasis added.

                                                                    1. 1

                                                                      Induction gives us a way to define larger and larger objects, by building them up; but we need to start somewhere (a base case). A classic example is the successor : Nat -> Nat which constructs a natural number that is one larger than its input; and zero : Nat is the base case we start with.

                                                                      Coinduction gives us a way to define objects by how we can “destruct” them into smaller parts, or alternatively by the ways that it can be used/observed. The interesting thing is that coinduction doesn’t need a base case, so we can define infinite objects like streams, or infinite binary trees, or whatever. We can still have base cases if we like, e.g. we can make a corecursive list with nil and cons, but in that case we can’t assume that every list will end in nil. As an example, recursive types in Haskell are coinductive: they might be infinite (they might also contain errors or diverge, since Haskell is unsound).

                                                                      Recursive (total) functions require a base case, since that’s the point where they return a value. Corecursive functions don’t require a base case, as long as they are “productive”, defining some part of the return value. For example, a corecursive function returning a stream can define one element and recurse for the rest; this will never end, but each part of the return value can be produced in some finite amount of time (i.e. it doesn’t diverge).

                                                                      AFAIK Python generators are inherently linear, like a stream; e.g. they can’t define an infinite binary trie like we could in Haskell (data Trie = Node Trie Trie). Another wrinkle is that Python uses side-effecting procedures, rather than pure, total functions; so we might want to consider those effects as part of the “productivity”. For example, we might have a recursive procedure which has no base case and never returns any value, but it causes some effect on each call; that can still be a useful thing to do, so we might count it as productive even though it diverges from the perspective of calculating a value. (I don’t think Python eliminates tail-calls, so maybe Scheme would be a better example for recursing without a base case, since it is then essentially the same as iteration)

                                                                    1. 3

                                                                      my previously answered thoughts on Dart and my previously answered thoughts on Flutter.

                                                                      Basically the language is not interesting but gives you shared code on client and server. I like the widget composition but the tooling to debug is not quite there, e.g. how do you look into failing HTTP requests? are there different tools for different environments? (still I haven’t looked into Flutter 1.0). It’s nice to have a reactive UI but Flutter is not the only framework that provides it (I guess?) so no bonus points.

                                                                      1. 2

                                                                        The formalization of passages using braid groups is super interesting but the best part are the videos of people collaborating with robots, especially the “failures” in which the operator goes “WTF you asked for help”