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 :)

                                                    1. 9

                                                      Upvoted on the title alone. The author makes some good points, but the talking point still stands alone.

                                                      1. 3

                                                        Don Syme wrote his thesis on finding an “unsoundness” in the Java type system back in the 90’s. I can’t seem to find his thesis right now, but this paper, “Proving Java Type Soundness” is based on that work https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/java.pdf

                                                        It was timely research. Microsoft was looking to create a Java alternative, and Don went on to work on .NET generics and become the creator of F#.

                                                          1. 7

                                                            There’s a lot of name-calling: imbecile, crackpot, etc. Wish the author could couch their skepticism in polite terms. I get it - over the years there have been all sorts of disproven free energy machines or what have you. THIS one has yet to be disproven, so I’d not go around slinging that language just yet.

                                                            If someone is able to figure out what is the cause of the force they measure, it may be interesting. But I can’t find enough motivation to spend a minute with this stuff because I am confident that whatever will be the actual reason why they think that they’re seeing a reactionless force, it will be dumb.

                                                            For now we have observations that do not fit existing knowledge, so why not investigate rather than dismiss? That’s all. I’m confident that they’ll figure out the mechanism of force generation as well, but I’m not as certain that it will be a ‘dumb’ reason. It may fit existing knowledge in some way, but show a novel application - which is totally ok. The point of the device AFAIK is not to prove ‘everything you know is wrong’, but rather ‘this might be useful, though we don’t understand how it works yet’.

                                                            Sadly news reporting tends to go towards the sensationalist ‘everything you know is wrong’ angle all too much, which perhaps the author is reacting to. I don’t know. But until we understand this EM drive I don’t see good reason to prance around calling everybody involved with it idiots.

                                                            1. 2

                                                              Disproving very simple things can take a lot of effort. However usually something valuable is learned if it isn’t simple instrument error. A gap in understanding here, an important fact there, and rarely a fundamental part of physics. Light wasn’t found to be a wave until someone was willing to do the dumb experiment to show how dumb it was to think that light could be a wave. Poisson really thought it was the STUPIDEST thing to insinuate. Sure this is very likely not that situation we are presently in but if we never tested we’d never actually know.

                                                              A little wiki excerpt. “Poisson studied Fresnel’s theory in detail and, being a supporter of the particle theory of light, looked for a way to prove it wrong. Poisson thought that he had found a flaw when he argued that a consequence of Fresnel’s theory was that there would exist an on-axis bright spot in the shadow of a circular obstacle, where there should be complete darkness according to the particle theory of light. Since the Arago spot is not easily observed in everyday situations, Poisson interpreted it as an absurd result and that it should disprove Fresnel’s theory.”

                                                            2. 2

                                                              fwiw, lubos is not particularly well respected in the physics community, so i wouldn’t consider him a good source of information.