1. 4

    Heck yeah! Always awesome to see another TLA+ enthusiast here :D

    My one nit here: while the time in TLA+ is essential complexity, we shouldn’t brush off time concerns as a serious cost. Complex models can take days or even weeks to run, and model optimization is a skill you have to learn to get really good at TLA+. That said, TLC is a pretty old model-checker and there’s been a lot of advances in model checking that could make it faster. I’ve seen some interesting proposals on offloading some computations to SAT or SMT solvers and then only switching to brute-force for the stuff they can’t do.

    1. 3

      Absolutely, I tried to still point that out. I’ve found that one hidden time cost of creating specs is in the debugging/iterating cycle. I’ve had a few times where I think the spec is at a good checking point and I run the model. Then I’m sitting waiting for 5 mins and have to decide on my own that this seems like way more states than it should be. This is not a problem you typically run into with a test.

      I haven’t really gone into the optimization part too much just yet since my specs are still pretty simple. It’s interesting that even, what feels like, the ultimate abstraction tool, is leaky once you try to do (e.g. model check) something complex with it. I guess there’s no escaping the law of leaky abstractions.

      Btw, thanks for Learn TLA! That’s what helped me bridge the gap from Specifying Systems to writing my own specs.

      1. 2

        Then I’m sitting waiting for 5 mins and have to decide on my own that this seems like way more states than it should be. This is not a problem you typically run into with a test.

        One trick that helps here is to define a TypeInvariant that makes bounded models a safety property. Something like

        TypeInvariant ==
          /\ counter \in [Servers -> 0..MaxCounter]
          /\ active \in SUBSET servers
        

        Then if the model has an infinite number of states, TypeInvariant fails and you catch the problem early. Another trick is to watch the state queue and model diameter in the “model results” page as its checking. If the diameter suddenly shoots up to 30 something’s probably wrong.

        Btw, thanks for Learn TLA! That’s what helped me bridge the gap from Specifying Systems to writing my own specs.

        Glad to help :)

      2. 1

        interesting proposals on offloading some computations to SAT or SMT solvers Specifically doing this from TLA+ ? I’d be interested in links, if you have any.

        1. 2

          It looks like I was misremembering a little. Most of the work in applying SMT to TLA+ are focused on the proof system. There’s Alloy Meets TLA+, where they used Alloy’s SAT translations to enumerate initial states for TLA+, but since then they’ve instead been porting TLA+ ideas into Alloy (that’s Electrum.) There’s also Apalache, which is trying to write a symbolic model checker for TLA+, but I’m unsure if they’re intending to replace TLC or just augment it.

      1. 1

        I would expect printing a cryptographic string in the classified section would be prone to errors, and even intentional manipulation, if the wrong people became interested.

        1. 2

          Completed a revamping of DependentTypes for F# yesterday, I think much more useful and includes dependent pairs. I still need to add tests of new functionality and document before I release.

          1. 6

            I nearly got the F# library XPlot converted to multitargeted net45/netstandard2.0, when I ran into the darndest problem. It builds fine in Visual Studio, but the build script fails in the build target on not finding the Newtonsoft.Json dependency.

            I’m sure I’ll figure it out this week. Here’s the branch, if anyone is interested. https://github.com/jackfoxy/XPlot/tree/magicmode

            1. 2

              Great post - I admit to being a bit curious to see those rspec macros too, even if it’s not a general approach.

              1. 5

                I don’t know about macros; but, I often generate tests from data in rspec. I too am curious what the macros bring to the table.

                I found this rspec truth table DSL too. It has a nice syntax…

                1. 2

                  I really wish I could share them, but it was at an old job and I don’t have the source code :(

                  1. 1

                    I don’t know about Rust. The matching in F# allows coding up sophisticated match situations. The compiler will tell you if you have left out a case. My favorite example is balancing a Red/Black Tree. This would be many lines of hard to understand imperative code:

                    type a t =

                    | Node of color * a * a t * a t 
                    
                    | Leaf
                    

                    let balance = function

                    | Black, z, Node (Red, y, Node (Red, x, a, b), c), d
                    
                    | Black, z, Node (Red, x, a, Node (Red, y, b, c)), d
                    
                    | Black, x, a, Node (Red, z, Node (Red, y, b, c), d)
                    
                    | Black, x, a, Node (Red, y, b, Node (Red, z, c, d)) ->
                    
                    	Node (Red, y, Node (Black, x, a, b), Node (Black, z, c, d))
                    | x -> 
                    	Node
                    
                  1. 6

                    The internet search experience suffered a setback when the major browsers abandoned the separate search box for the combined address/search box. Only FireFox retains this feature, where your default search engine is the first choice in a list.

                    In the days before Alta Vista became better than Yahoo, and then Google crushed all other search options, there were meta-search engines that combined, filtered, and formatted results from several search engines of your choice. IIRC Magellan was one of these. I’ve toyed with the idea of reviving this idea for my own use. Google and Bing are pretty similar, but not perfectly similar, and provide different results depending on whether you are signed-in or anonymous. DDG usually provides different enough results to be important. There’s a lot of room for innovation in meta-search.

                    Finally there are still all sorts of specialized search options. In this category I would start with Amazon and Wikipedia. There are also sites like noodle.com, specializing in education related searches.

                    1. 5

                      DuckduckGo is my go to search.

                      It is simple and doesn’t have the Google bloat to it and thise smart searches like where you can generate a md5 hash for example in a search query or do number system conversions is pretty cool

                      1. 2

                        Duckduckgo owns, its my configured default search on all devices. When i need something specific from Google, i use the bang feature for google, !g.

                        1. 2

                          I never knew that was a bang available, my word. Is there a !b for bing too? (Update: there is wow)

                        2. 0

                          So essengially DDG has a great interface and is actually way more useful.

                          1. 4

                            Let’s be honest, though: the results are not as good as Google for many/most queries.

                            1. 3

                              I don’t know. I switched to DDG at home and I’ve always been able to find what I’m looking for. I still use Google at work so I’m able to compare and contrast. About the only place where Google is better (in my opinion) is in image search, and that may be due to how Google displays them vs. DDG.

                              1. 4

                                Here’s a concrete example. Let’s say I’m trying to remember the name of the project that integrates Rust with Elixir NIFs.

                                First result for me for the query “elixir rust” on Google is the project in question: https://github.com/hansihe/rustler

                                After scrolling through three pages of DDG results, that project doesn’t seem to be listed or referenced at all, and there are several Japanese and Chinese-language results despite the fact that I have my location set to “United States”. I will forgive all the results about guitar strings since DDG doesn’t have tracking data to determine that I’m probably not interested in those (although the usage of the word “rust” in those results is in the term “anti-rust” which seems like a bad result for my query).

                                That query is admittedly obtuse, but that’s what I’ve become accustomed to using with Google. These results feel generally characteristic of my experience using DDG. I end up using the !g command a lot rather than trying to figure out how to reframe my query in a way that DDG will understand.

                                1. 2

                                  I think you did that wrong. You were specifically interested in NIF but left that key word off. Even Lobsters search engine, which is often really off for me, gets to Rustler in the first search when I use these: elixir rust nif. Typing it into DDG like this gives me Rustler at Page 1, Result 2.

                                  Just remember these high-volume, low-cost engines are pretty dumb when not backed by a company the size of Google or Microsoft. You gotta tell them the words most likely to appear together. “NIF” was critical in that search. Also, remember that you can use quotes around a word if you know for sure it will appear and minus in front of one to eliminate bogus results. Put “site:” in front if you’re pretty sure which place or places you might have seen it. Another trick is thinking of other ways to say something that authors might use. These tricks 1990’s-early2000’s searches get me the easy finds I submit here.

                                  1. 0

                                    I disagree that “NIF” was essential to that query. There are a fair number of articles and forum posts on Google about the Rustler library. It’s one of the primary contexts that those two languages would be discussed together. DDG has only one of those results as far as I see. Why? Even if I wasn’t looking for Rustler specifcally, I should see discussions of how those two languages can be integrated if I search for them together.

                                    1. 2

                                      There are a fair number of pages where Elixir and Rust will show up without Rustler, too. Especially all the posts about new languages. NIF is definitely a keyword because you’re wanting a NIF library specifically instead of a page about Rust and Elixir without NIF. It’s a credit to Google’s algorithms that it can make the extra connection to Rustler pushing it on the top.

                                      That doesn’t mean I expect it or any other search engine to be that smart. So, I still put every key word in to get consistently accurate results. Out of curiosity, I ran your keywords to see what it produces. The results on the top suck. DuckDuckGo is usually way better than that in my daily use. However, instead of three pages in, DuckDuckGo has Rustler on page 1, result 6. Takes about 1 second after hitting enter to get to it. Maybe your search was bad luck or something.

                                  2. 1

                                    I did exactly that search and found it at the 5th position.

                                    While “elixir rust github” put it at 1st position. Maybe you have some filters? I have it set to “All Regions”.

                                2. 2

                                  Google has so many repeated results for me that I feel they have worse quality for most of my queries than ddg or startpage. Maybe I’ve done something wrong and gotten myself into a weird bubble, but these days I find myself using Google less and less.

                                  1. 1

                                    Guess so. I have been using it at uni though for a long time and gotten atleast what I needed.

                                    But I admit that googs has more in their indexes.

                              2. 5

                                Searx is a fairly nice meta search engine.

                                1. 4

                                  Finally there are still all sorts of specialized search options. In this category I would start with Amazon and Wikipedia.

                                  DuckDuckGo has a feature called “bangs” that let you access them. Overview here. Even if not using DDG, their list might be a nice reference of what to include in a new, search engine.

                                  1. 1

                                    the URL bar itself now performs a search when you put something that’s not a URL in it

                                    1. 1

                                      I thought that was clear. What I like about the old style dedicated search box is it that its is so easy to switch between search engines.

                                      1. 3

                                        I believe that you can use multiple search engines in an omnibar by assigning each search engine a keyword, and typing that keyword (and then space) before your search.

                                        1. 1

                                          Or if you use DuckDuckGo, you can use !bangs to pivot to another search engine or something else.

                                        2. 2

                                          With keyword searching (a feature I first used in Opera, and which is definitely present in Firefox; I can’t speak to any other browsers), it’s “so easy” to switch between search engines—in fact, far easier than with a separate search box. I type “g nephropidae” to search Google, or “w nephropidae” for Wikipedia, “i nephropidae” for image search, or even “deb nephropidae” for Debian package search (there’s no results for that one).

                                          1. 2

                                            This is not completely obvious from the user experience. Without visual cues, much available functionality is effectively hidden. You must have either taken the initiative to research this, someone told you, or you stumbled upon it some other way. This also effectively requires you to have CLI-like commands memorized, the exact opposite of what GUIs purport to do. And adding new search engines? That’s non-obvious.

                                            1. 1

                                              I use YubNub to get large library of such keywords that is the same on every device.

                                      1. 2

                                        I took a stab at this problem by sourcing bits from a random quantum source to generate different sized signed/unsigned integers, ranges of integers, etc.

                                        https://jackfoxy.github.io/RandomBits/

                                        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?