1. 3

    I’m now a maintainer on this project https://github.com/fsprojects/FSharpx.Collections Working on a 2.0 release of the project which will include implementing the libraries in netstandard2.0 and converting all the unit tests to Expecto

    1. 8

      The main problem of official twitter client and website is not ads (there are few ads and with not so poor quality), but facebookisms: out of order timeline, tweets from users I’m not subscribed to (just because someone liked them), “who to follow”, putting “trends” consisting of junk news in front of my nose.

      1. 2

        I would gladly put up with slightly more adds in exchange for fixing all these things, and giving me a more advanced filtering mechanism.

        1. 3

          I would pay a small monthly fee to have all those things with no ads.

      1. 3

        Voevodsky and Lamport both recognized the problems with verifying proofs and both advanced the state of the art, in different, yet complimentary, ways: HoTT and TLA+.

        1. 1

          Converting an existing F# solution (2 projects) to the new project file and msbuild system. Partial success so far, one project now builds.

          In other news, still trying to get the current master on the FSharp.Formatting repro to build AND generate output files. The maintainers have been updating master for a year and a half now since the last official release and at least for the last 14 months the built software will not generate output files. I now know why, but the parties involved have been uncommunicative about how they intended to go forward with their changes.

          1. 1

            Happily the maintainer got back in touch with me right after I wrote this. Hope to make more progress this week.

          1. 5

            Tryin to get F# Azure Functions working. Then the plan is to switch again to learning TLA+.

            1. 3

              continuing working on dependent typing for F# https://github.com/robkuz/robkuz.github.io/issues/6

              1. 3

                Awesome! I have been wanting to do something almost exactly like this for a very long time, and it looks like O’Connor did a great job. They even did the thing where you identify unapplied sub-expressions with known computations and call out to an optimized C version, although their version is more elegant than what I was thinking (calling functions by hash rather than by value).

                1. 1

                  I only recently got interested enough in blockchain to start really learning about it, reading the technical papers, etc. High on my list of problems to solve was formal verification of contracts. I think this paper knocks it out of the park, although admittedly there may be other contenders in the literature I don’t know about.

                  The company O’Connor is with, Blockstream, looks to me like a leader in “figuring stuff out” for blockchain. I also like their sidechains proposal, https://blockstream.com/technology/sidechains.pdf, it is not a complete solution and the paper points out several problem areas. The company is a backer of the Elements Project https://elementsproject.org/ which experiments with sidechains.

                  I also just found a Confidential Assets paper by people in the company, https://blockstream.com/bitcoin17-final41.pdf, I have not read yet.

                1. 4

                  This article reads like one of those ClickHole satires where the author can’t stop inserting random interjections into an otherwise normal story. It has almost nothing to do with the history of zero; that is just a disposable vehicle for the author’s directionless political ramblings.

                  1. 3

                    Yeah, the NatGeo piece to which it links is considerably better and not filled with political frivolities: http://news.nationalgeographic.com/2017/09/origin-zero-bakhshali-manuscript-video-spd/

                    1. 1

                      As I often do, clicking to the comments first… (Now not going to read the article.) Must politics intrude on everything? Even an article with the math tag? More anecdotes feeding my confirmation bias about the NY Times is not making me a better person.

                    1. 5

                      A decent read, and I learned more about DNS. That fact that I actually prefer email for communication with my friends helps me appreciate the content, although most of them don’t use it much. (Hrm, maybe that says more about me than my friends…)

                      But given how complicated it is to setup what is mentioned in the article, I don’t hold out a lot of hope that this will become the norm.

                      1. 5

                        No, it’s not you. Email has fallen out of favor because it has not advanced beyond Gmail. I think spam is mostly to blame. You should have at least one whole domain to invent new addresses from. This would allow “you” (and really I mean with software assistance) to manage burner addresses and addresses for specific purposes.

                        1. 4

                          That’s exactly what I’ve been doing extremely happily for the last ~15 years. A completely separate domain with a few category-styled mail aliases to one mailbox which all accept + suffixes on the local part, which I fill in with the domain name of the service I’m giving the address to. Great indeed to manage burners and specific purposes, but also lets you watch who sells or otherwise lets slip your email address, vs. who doesn’t.

                      1. 7

                        This is a thought I’ve been having for a year or so, that email really is the original social media. There’s still a lot of room at the bottom to personalize IMAP. GMail kind of took over that space, took it to a certain level, and then stopped. It seems like no one else is going to bother continuing. It is on my too long list of things to do.

                        1. 9

                          It seems like no one else is going to bother continuing.

                          Because Google is going to kill any interesting extension to IMAP by not supporting it for @gmail.com. Because Google along with other big players is now clenched in a delusional “war” to lock down users in their own messaging walled gardens, and none of them is interested in supporting anything open at the moment. Fortunately they can’t outright kill email because its user base is bigger than all the rest of messaging combined. It’s the only communication method that actually works for everyone on the Internet.

                          This is, by the way, why XMPP died. I used to be able to talk to @gmail.com addresses over it but then Google simply killed federation citing some mumbly non-reason.

                          1. 2

                            BTW, XMPP federation with Google still works (if the Google user is using Google Talk – which mostly you access with third party clients these days, since they no longer maintain any of the official ones). Several of my many XMPP contacts are @gmail.com addresses and I talk to them this way every day.

                            1. 2

                              You’re the lucky one then :-) All of my contacts have dispersed over facebooks/twitters/imessages.

                          2. 7

                            I recently discovered delta.chat as a fun alternative IMAP UX for chats

                            1. 1

                              I remember several years ago someone launched a similar chat interface. I can’t remember what it was called though. But this is definitely interesting.

                              1. 1

                                delta.chat

                                That’s pretty brilliant. A combo of that, end-to-end crypto, and Keybase.io-style discovery could be interesting. I’d say chat messages should probably be in their own folder(s) to avoid cluttering up the main inbox, though.

                                1. 2

                                  By default delta.chat stores chats in a Chat folder and uses OpenPGP when it can detect support using Autoencrypt

                              1. 6

                                I can highly recommend the TLA+ video course, if only for the nice outfits of Leslie.

                                http://lamport.azurewebsites.net/video/videos.html

                                1. 5

                                  I’m a fan of the video course too, but having said that it will not actually teach you TLA+. For that you really need to study the book and the sample specs in the toolkit, but after the first 2 short (and delightful) videos you will have an understanding of what TLA+ is and what it (might) be useful for. The next 2 videos give you a deeper look.

                                  1. 1

                                    What book could you recommend about TLA+?

                                    1. 3

                                      Lamport’s book, https://www.microsoft.com/en-us/research/publication/specifying-systems-the-tla-language-and-tools-for-hardware-and-software-engineers/ , Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers , also available as a free PDF.

                                      1. 2

                                        One major limitation of Specifying Systems is that it was written in 2004, so it misses some of the more modern features of TLA+, like PlusCal, recursive operators and lambdas, and TLC debugging tools.

                              1. 2

                                Looking forward to a ledger that allows participants to (1) make a data-stream (of some type) available to a subset of privileged observers, (2) weight these streams (3) block and distribute based on weight, (4) allow network participants to chain streams into new “types”

                                1. 1

                                  Curious: what is the use case for such a system?

                                  1. 3

                                    Apparently smart contracts. Coincidentally a friend just last week recommended I read up on Tezos. Take a look at the Michelson language specification in particular. https://www.tezos.com/static/papers/language.pdf

                                    1. 1

                                      Just found this, appears to be a primer on Michelson, but I haven’t looked too closely. https://www.michelson-lang.com/

                                    2. 1

                                      Enterprise integration, actually. Working on a paper, but don’t hold your breath.

                                  1. 2

                                    After a couple of weeks of mostly tedious research to become more proficient at Azure devops, finally moving on to Azure F# functions and work with Azure queues.

                                    1. 2

                                      Well…seems I’m sucked back into Azure devops. I got a reply to an outstanding S.O. post of mine, https://stackoverflow.com/questions/45662890/azure-powershell-add-azurekeyvaultmanagedstorageaccount-failing , and I’m still trying to make it work.

                                      Am I the only one who feels like an idiot trying to figure out Azure RBAC?

                                    1. 1

                                      Writing a binary search was one of the first things taught when learning COBOL and IBM 370 Assembler back in the day. I’m pretty sure I implemented it at least once in each language. What I really wrote numerous times for implementation was bubble sort. There were no handy framework DLLs to call back then.

                                      1. 7

                                        First week laid off my job, so time to get serious about my personal server project. Continue learning TLA+ and develop story map for the project.

                                        1. 6

                                          Condolences on the layoff. :(

                                          Remember, you’re worth more than just your job! :)

                                          1. 2

                                            Sorry to hear about the layoff. That sucks If you’re in the US, make sure you grab that unemployment claim.

                                          1. 8

                                            Writing my first TLA+ spec.

                                            1. 4

                                              glee

                                              Feel free to message me if you run into any problems!

                                              1. 3

                                                …are you Leslie Lamport?

                                                1. 4

                                                  No, but I’ve written a ton about it and Lamport is a lot busier than I am.

                                              1. 6

                                                Good article, but one super minor nitpick: “ampersand” is &, not @. There isn’t an english term for @ outside of “at sign”.

                                                1. 4

                                                  There isn’t an english term for @ outside of “at sign”.

                                                  AT SIGN, at, each, vortex, whirl, whirlpool, cyclone, snail, ape (tail), cat, snable-a#, trunk-a#, rose, cabbage, Mercantile symbol, strudel#, fetch#, shopkeeper&, human&, commercial-at, monkey (tail)

                                                  1. 1

                                                    Embarrassing faux pas in article now fixed. Thanks for pointing this out. I know the difference, but somehow my brain was down a wrong path when I was working on this article.

                                                  1. 7

                                                    i tried. i really wanted to like it, but the tooling and dev environment under linux is still pretty miserable, and to make matters worse, all the blog posts and tutorials seem to assume you’re using visual studio.

                                                    (if someone wants to play with it, i started a project to make life a little easier)

                                                    1. 3

                                                      We’re an F# shop, and we have 1 guy learning F# using VS Code / Ionide in Linux exclusively. Frankly, he is kind of struggling without the good debugger in Visual Studio. Ionide has the advantage of being “light weight”, and I use it daily for some purposes, but the debugger and better intellisense in full VS just make the experience so much better.

                                                      1. 3

                                                        Is the project targeting Mono or .NET Core? If they’re using Mono, there’s a plugin that provides decent (but admittedly not amazing) support for the Mono debugger.

                                                        1. 1

                                                          Mono. Thanks, I’ll mention that to him.

                                                    1. 4

                                                      I’m curious if anyone is knowledgeable about how ad blockers and software like Brave browser fit in with the terms of use situation. Seems like if you are crawling and scraping for your own personal use, and not re-publishing, you might be able to craft your crawler/scraper to adhere as closely to TOU as ad blocking does.

                                                      1. 3

                                                        Brave is in a very precarious spot I think because they’re taking the content, remixing it, and showing it. That’s close to what aereo was doing. Actually probably more infringing than aereo. Maybe you can do it for yourself, personally, but it’s treacherous ground for a business model.

                                                        1. 2

                                                          I’m curious if anyone is knowledgeable about how ad blockers and software like Brave browser fit in with the terms of use situation.

                                                          Personally, I don’t know. It’s a different topic.

                                                          But if you consider that there are still a lot of grey areas in law about scraping/crawling, there are probably also a lot of grey areas about Ad Blockers. I’ve just googled it and I found that some German publishers sued Adblock Plus in the past. Not sure what happened to the other ad blockers.

                                                          Seems like if you are crawling and scraping for your own personal use, and not re-publishing, you might be able to craft your crawler/scraper to adhere as closely to TOU as ad blocking does.

                                                          I don’t think so. Because ToS/ToU often prohibit automatic data collection.

                                                          1. 2

                                                            But if you consider that there are still a lot of grey areas in law about scraping/crawling, there are probably also a lot of grey areas about Ad Blockers. I’ve just googled it and I found that some German publishers sued Adblock Plus in the past. Not sure what happened to the other ad blockers.

                                                            AdBlock Plus has an “acceptable ads” product, which charges larger publishers a fee to be included on that list.

                                                            https://adblockplus.org/acceptable-ads#revenue

                                                            Springer sued AdBlock Plus and ad blocking itself was deemed legal, “acceptable ads” not.

                                                          2. 1

                                                            There have been plenty of attempts by publishers to sue adblockers with arguments along those lines. From what I’m aware they always lost.

                                                            1. 1

                                                              Apparently, Google and other big names attempted to sue Adblock Plus. But I don’t know how it turned out either.

                                                              It would be interesting to do a bit more research on this topic. What we’d find out would probably be super interesting :)