1. 7

I do like Eric’s definition of pragmatic and conservative programmers. I am definitely a conservative programmer who felt compelled to learn F# back in 2010, when I decided to myself functional languages were the future of software engineering. Only later did I figure out strong typing was just as important as the functional aspects for writing “correct” code (for some definition of correct). I’ve been working exclusively (the habit of conservative programmers) in F# and SQL for the last 5 years. The last 2 were very painful, as Microsoft turned everything upside-down in the transition to .NET Standard/Core. That pain is pretty much in the past now. Visual Studio is finally stable for F# (albeit I’m looking forward to editor performance improvements in the next major release). The transition to FAKE 5.0 was largely a fiasco. I felt like an abused beta-tester, as each new release broke something new, but together with the recently released BlackFox.Fake.BuildTask library FAKE is now a better make DSL than ever. .Net Standard 2.1 is stable and growing, Azure is mostly stable and useable, Visual Studio is stable (or use Ionide in VS Code or Rider). Don Syme and the Microsoft F# team (who I all know) have done a great job keeping the language on track. Now is a great time to get into F#, if you are so inclined.

1. 2

I just wanted to say that I’ve really been enjoying these posts and the book. On the other hand, the experience of working with the tla+ tooling has been less great. I’d really prefer cli+editor, and there doesn’t even seem to be a canonical emacs mode for tla.

Is there some other way of interacting with the system? Or another tool focused on concurrent systems that doesn’t come saddled with the uncomfortable and inflexible environment?

1. 6

I feel your pain. IMO terrible UX is the biggest problem with TLA+ right now. It doesn’t help that Lamport doesn’t want it to change, and is generally against improvements like REPLs or CLIs.

You can get the jar for running it on the command line here. I tried running TLC from the command line and it always threw a null pointer error unless I called out from a vim buffer. ¯_(ツ)_/¯

Re other tools, SPIN is super old but works from the CLI, and Alloy has a full API and language server. I know about Storm/PRISM and B but haven’t investigated either of them.

1. 3

Is Lamport actively opposed to new tools, or just does not want to see the tool set he works with changed? Naively it seems like there is enough information out there for someone ambitious enough to create a new IDE. VS Code would be a likely host.

1. 1

Thanks for this link. I’m reading your book and I too would prefer cli + vim, but I’m currently using the tooling you specify in the book (and even that was a pain to install [wrong Java version]!).

1. 3

Understanding CTEs was a revelation for me. For me it is so much easier to compose a non-trivial query from custom sets built with CTEs as opposed to sub-queries, which tend to get cluttered and don’t stand out as obviously to my perception as set building blocks.

1. 2

Recursive CTEs are also very cool. They somewhat remind me of “unfolds” or “anamorphims” from functional programming, in that they start from and initial “seed set” of rows and add new rows by repeatedly applying a query to the results from the previous step. https://stackoverflow.com/questions/3187850/how-does-a-recursive-cte-run-line-by-line/3188127#3188127 Maybe they should be called co-recursive CTEs instead!

1. 3

We use recursive CTEs at work to traverse graph structures that we store within the database. It’s really neat, but also a performance nightmare. For large tables, recursive CTEs have a tendency to hold a lot more stuff in memory than they need to. This has caused lots of unintuitive problems for us e.g. our database running out of space because a large recursive CTE query ate up a ton of memory, swapped it all to disk, then timed out and never cleaned the swap files up.

1. 1

What database engine are you using?

1. 1

We’re running on PostgreSQL.

1. 2

I just requested Dec 28.

1. 1

1. 1

I’m not working on any personal projects this week.

But I will give myself a plug for something I wrapped up last week, a big upgrade to F# Dependent Types (yeah, yeah, yeah, not for formal methods, but for type granularity). Now a greater range of base types, and Dependent Pairs. https://jackfoxy.github.io/DependentTypes/ most interesting parts in tutorial.

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.

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.