1.

I promised deep feedback and then completely forgot to follow up on it, I’m the worst friend D:

Nonetheless like how the final article turned out! Tbh it’s probably better than it would have been if I’d thrown you my obsessive writing pedantry.

1.

I’m confused why on a list of only five things to learn — among the incredible amount that any developer could learn — two of the recommendations are virtual DOM diffing engines.

Maybe don’t keep learning the same thing over and over with syntax swaps.

Maybe learn something new.

1.

With a little digging, it becomes kinda obvious. This is somebody farming lobsters for traffic.

1.

Now I’m wracking my brain on how to write a good and informative “5 things to learn” satire

1.

Seeing this on Hackernews, it reinforced my feeling that ordinary philosophy is kind of weird.

I would look at a model-theoretic equivalent. Suppose you have a model and an axiom systems. You might incorrectly prove a given theory that is actually independent. But it might actually be the case that you working with a model within which that theory happens to be true. This seems like the analogue of the “justified belief that isn’t knowledge” examples. The thing here, is that you easily fill in the “hole” by specifying that one’s justifications have to be correct.

And altogether, it is surprising that philosophy didn’t put the constraint on “justified” to meaning “a fact that makes another statement true” rather than it being a fact that merely convinces some people.

I suppose the problem is philosophy is dealing with less certain situations and the philosopher is trying to come up with a compact piece of rhetoric that would convince another human rather than engaging automatable process.

1.

That raises questions about what a “justification” is, and what it means for a justification to be “correct”. Epistemology deals with messy questions of understanding and knowledge. I know I’m going to drink water tomorrow. My justification is that every day for my entire life, I drank some water. But inductions make terrible justifications: I could die in my sleep. So the justification is not correct, and yet I still know I’m going to drink water tomorrow.

1.

It’s your file system. This is really low effort clickbait content…

1.

I think the author does something interesting with it. I thought the article was gonna be able how NoSQL is “natural” or “intuitive” or something, but it was actually about how we hold data to a different standard than code.

1.

I’d definitely recommend reading the original paper, which is linked in the article. IMO Case 2 is a more interesting and persuasive example than Case 1 (which the article uses).

I’m also a little obsessed with Gettier Problems. Here’s a one I really like:

• Bob makes empirical claim X, and cites papers A, B, and C.
• A, B, and C each cite another two papers as empirical evidence for the claim.
• All six of the second tier papers cite a single originating source, Q, which was written by a giant in the field.
• In the forward of Q, the author says the claim X is from a thought experiment and not empirical at all.
• Unrelatedly, there’s an obscure paper R nobody read which does a controlled study and finds evidence supporting X.

Does Bob know X is true? He has nine papers supporting him, so he’s certainly justified! And there’s a tenth paper he doesn’t about which actually confirms X, so it’s definitely true. But is it knowledge?

This kind of problem comes up a lot when doing software history or empirical engineering.

And here’s one from formal methods: you prove your code will sort a list and use a correct theorem prover to verify the proof. Unkown to you, your production environment has a wonky CPU bug that makes the sort function give incorrect outputs for certain classes of inputs. In your problem domain there’s never a case where you will ever need to input something that would trigger the bug. Is your sort function always correct? Do you know this?

1.

What I think people are missing in this debate are the tech companies are salivating.

What a marvellous unending revenue stream…

…sure they are being forced to hand over their users data…

…and they will howl and cry about that to the press…

…all the way to the bank.

Each search request will be done… for a fee.

At a neat profit.

What a scam!

Charge the user to hold their private data…. and then sell it to the highest bidder (boohoo we didn’t want to they forced us boohoo weeheeeheehee).

And guess what, I bet the government won’t always be the highest bidder.

1.

I don’t see how that’s the case. It sounds like the Australian government wants to force companies to give them data. They’re not paying for it.

1.

The US government does something similar. Yet, the telecoms charge the LEO’s a fee for some kinds of access. cryptome published them at one point. It was several, hundred dollars leaning toward a thousand for cellphone companies if I’m remembering right. They even had a web portal for it. Comcast also billed for the pen register taps.

1.

Want a bet?

Yes, they will be forced to cough up the data… but I bet they can impose a fee for each search.

I believe they already do so, for example, on all cell phone record requests.

And even if it the fee isn’t line item on the bill just passed, I will bet you a six pack of something cold that a court challenge would succeed.

Not to dismiss the bill, that won’t happen, but to force the government to re-imburse the tech companies for the, cough, “costs” incurred.

Infrastructure manufacturers are also salivating… these “back doors” are a Premium Feature which command Premium Prices.

And they will get it.

Paid for by the taxpayer.

I would love to see the treasurer advice on this bill… I suspect they will have already budgeted for these costs.

2.

I also don’t like that law but I think you’re unnecessarily outraged by that (potential) fee. I’d assume the demand for data access is a decreasing function of the price. The more expensive they are the less likely the government is to ask for them. So the no-fee scenario is one with the maximum number of requests. I doubt that’s your intended goal.

Regarding the regulation, please have a look at the official document. I haven’t read the whole thing but here are some highlights (emphasis mine):

Schedule 1 of the Bill will provide for industry assistance, which can be voluntary (a technical assistance request) or ordered (a technical assistance notice or technical capability notice). […] The assistance provided by a designated communications provider would be in the form of technological assistance and include, but not be limited to: removing electronic protection; providing technical information; formatting information; and facilitating access to devices and other things.

The key amendments in Schedule 2 of the Bill relate to computer access warrants. These warrants permit covert access to data held in a target computer (which is broadly defined and may include more than one computer networks or systems). The amendments will:

• expand the powers available under computer access warrants and authorisations executed by the Australian Security Intelligence Organisation (ASIO), including by allowing ASIO to intercept a communication for the purpose of executing a computer access warrant and undertake activities to conceal access after the expiry of a warrant
• introduce equivalent computer access warrants for law enforcement agencies under the SD Act and
• make related amendments to the Mutual Assistance in Criminal Matters Act 1987 and the Telecommunications (Interception and Access) Act 1979.

Schedule 3 of the Bill will clarify and enhance the ability to collect evidence from electronic devices under warrant, by allowing the collection to occur remotely. Amendments will enable law enforcement to access information associated with an online or web-based account.

Schedule 4 of the Bill will bring the search warrant powers available to Australian Border Force (ABF) officers under the Customs Act 1901 into closer alignment with those available to police under the Crimes Act 1914.

Both Schedules 3 and 4 will expand the situations in which law enforcement officers may obtain an order requiring a person to provide assistance (such as authentication on a device), or risk a custodial sentence and/or a significant financial penalty.

1.

I’m outraged by the perverse incentives at work and the dishonest two facedness.

With one face displayed to their customers they moan and wring their hands…

…with the other face they are lobbying for the business.

Your highlighted sentences miss the point.

Yes they are required by law to expose the customers data, this gives them “plausible deniability”, “it’s not our fault”.

But I think you will find another law elsewhere that says the government must pay for services rendered.

Because of the controversial nature of this law, they have kept the two sides at arms length.

If we had any real journalists left, that is what they would be looking for… who in the business community is (quietly) lobbying for and championing this law.

I think you will find the “no fee” scenario is best…. it will be fought tooth and nail and dragged through court and delayed because the telco’s will lose money on every request.

But the history of military budgets shows the price is remarkably poor at effecting demand. ie. It all comes out of some big bucket of other peoples money.

1.

Regarding my highlights: I wanted to emphasize other aspects of this law that seem to be eclipsed by encryption regulation. For example, if my understanding is correct, the last highlight means the law will require you to provide the password to your device or risk penalty.

It seems by “demand” you mean “total amount spent” but I mean “total number of services rendered”. If military suppliers slashed the prices of equipment in half would the government react by reducing the budget in half or ordering twice as much? I’d say their response would be closer to the latter option. I think the same principle applies to the fee you mentioned.

It doesn’t matter that it’s other people’s money. If the budget is 10M and one unit costs $100k then you can buy 100 units. That’s maths. If you slash the price in half then the same 10M can buy 200 units. Also, I’m not sure whether my reading of the document I linked is correct but it seems their intent is to go after all companies in the world even if not present in Australia. Relevant passage: A failure by a designated communications provider (other than a carrier or carriage service provider) to comply with TAN or TCN requirements will attract a maximum penalty of 47,619 penalty units (currently$9,999,990) if it is a body corporate; for other providers it will be 238 penalty units (currently $49,980). […] Issue: conflict of laws The DIGI submission noted that the Bill ‘makes explicit its intended reach beyond the borders of Australia to any technology provider with a connection to Australia’. It considered that this ‘causes major problems for businesses and it could ultimately put Australians at risk’: […] Additionally, Apple’s comment seems to interesting. I haven’t read the law itself but if that comment is accurate then the law is written in extremely broad terms (emphasis mine): We encourage the government to stand by their stated intention not to weaken encryption or compel providers to build systemic weaknesses into their products. Due to the breadth and vagueness of the Bill’s authorities, coupled with ill-defined restrictions, that commitment is not currently being met. For instance, the Bill could allow the government to order the makers of smart home speakers to install persistent eavesdropping capabilities into a person’s home, require a provider to monitor health data of its customers for indications of drug use, or require the development of tool that can unlock a particular user’s device regardless of whether such [a] tool could be used to unlock every other user’s device as well… While we share the goal of protecting the public and communities, we believe more work needs to be done on the Bill to iron out the ambiguities on encryption and security to ensure that Australian are protected to the greatest extent possible in the digital world. 1. 26 The original group wrote a response here: Speed Without Wizardry 1. 1 The counter is also a respectful one that highlights the other person’s good points and skill. Loved reading it. 1. 7 This is fascinating and I’d love to see more data about it. It mirrors my observations that, for example, these days the youtubers who actually make money off their channels don’t do it from Youtube ads (which uBlock Origin blocks quite nicely, and thank Eris it does), but make it either from Patreon, in-band sponsorships (a quick blurb as part of the video), or both. 1. 7 In my personal experience, I can’t remember ever buying something from a banner ad, but bought plenty of things from affiliate links or plugs. 1. 2 I have bought one thing from a banner ad. It was a mistake. Garbage product. 1. 2 A lot of recent posts are about how duplicating code isn’t so bad. The empirical research agrees: most of the time when people copy-paste code, they’re doing it in a way that makes the codebase better off than if they tried to add a new abstraction. 1. 9 I’m delivering a 5-day TLA+ workshop next week and in the process of radically restructuring everything to better teach the mental models. As part of this process I’m writing a lot of beamer and tikz slides, which means hitting all sorts of weird beamer and tikz quirks, which means shaving many, many yaks. Unrelatedly, writing Practical TLA+ errata. For personal stuff I’m starting to feel the pain of not having a good exobrain, so more work on that. Probably set up a research notebook system. 1. 2 Let us know what you land on for that exobrain :) 1. 2 I’ve been using Zotero for a while now to store citations and their attached documents (PDFs, full webpages, etc. all get stored in a Zotero SQLite DB). With the browser plugin, it’s usually one click to import a citation and its attached document. Zotero also supports fully-searchable tags and notes. In retrospect I should have probably set up the online syncing sooner. For more unstructured notes I use the Mac OS Notes app. My complaint with both apps is their default notes font is too small. 1. 2 Zotero looks great! I’ve been feeling overwhelmed at the amount I reading I plan to do this year. This should greatly help in keeping it structured. Just installed it. 2. 1 where is that TLA+ workshop being delivered? That sounds interesting to me… 1. 1 Chicago! David Beazley’s been a great mentor to me. 2. 1 I ended up, after too much thinking about research notebooks, with a template text file. The app that wasn’t 1. 15 Welp, guess Github just lost my business (because the one thing I was paying for is now free) 1. 13 I’d wager that most of GitHub’s income comes from companies who host their stuff there. I just checked, and we pay$1,182/month to GitHub. The few people that had \$7/month subscription probably isn’t really worth it, as private repos are free on a number of other providers.

In the long run, it might even be beneficial for GitHub’s income, as the more people that use GitHub for their personal stuff, the more likely they’ll be to use/recommend it for their business, too. Atlassian does something similar with their pricing for most products: it’s very cheap for small teams (<10 people), and then a massive price-hike if you’ve got more people.

1. 4

Most of GitHub’s income comes from enterprise users. This is generally true of every company with an enterprise offering, but we know it from a 2016 Bloomberg article (analysis). It’s reasonable to estimate GitHub’s personal plan was a single-digit percent of its revenue and only marginally profitable because of support.

2. 5

Usually works out the other way. That’s funny.

1. 4

Maybe it will work the other way around: Everyone moves to MSGithub now, and next year they start charging for private repos. :-)

1. 7

But everyone (basically) is already on MSGitHub. If anything this seems like an attempt to build goodwill. Maybe they’re a little concerned about the growth of alternatives as well. But I doubt they were making very much off of individuals paying for five private repos. The big money is in the corporate contracts.

1. 1

Good thinking. :)

1. 7

I haven’t found the time to write as many blog posts as I’d like, so feel free to be brutal constructive with any feedback. The site is also still not finalized, e.g. I know the side-nav is kinda annoying.

1. 8

I would argue that even C is probably not a good starting language and something like Go would better suited for a beginner programmer course. Go has far less surprising behavior than C let alone C++. Initialization as an example since that was the point of the article is extremely well defined in Go with everything having a zero value.

The value of C is probably in learning how badly you can accidentally shoot your foot off and you’ll still spend far more time learning the gotchas than you will the computational science that you wished to learn.

1. 9

I wholeheartedly agree with you. It seems that most universities have switched to Python, but I still think Python has too many distracting features. I like the idea of teaching something like Racket instead, where the focus is really on decomposing problems and functional composability, a skill I wish more had by the time they reach C. There’s even graphics support.

Given that, C can produce a natural gradient to more in-depth systems programming concepts. For example, you get a segfault. “What’s a segfault?” Now we can introduce concepts of virtual memory, paging, et al.

1. 3

Racket would be great, it has a lot of useful stuff in the standard library, great documentation, a good IDE…

Unfortunately I think many people would still take issue with the damn parentheses. Maybe it would be worthwile to develop a #lang in the vein of ReasonML that looks closer to an ideal C/JS-like lingua franca, such as sweet-expressions

1. 1

Our professor that taught us in Racket also taught us the useful hotkeys in DrRacket to deal with parens. It ends up not mattering at all, with just a tiny bit of effort.

1. 1

What about something like pyret? It was written by racketeers originally as a racket #lang and only later became its own language.

2. 1

I mean, this is the pedagogic approach of SICP, but even MIT has moved away from it. We used it in my CS classes at Chicago, too, but that was back in the paleolithic era (1990).

It always made sense to me to start from the principle of handling abstraction, before moving onto actual computer stuff; but then, how much of that is confirmation bias on my part?

1. 7

I feel like it’s worth mentioning that some people feel like using Beamer is a bit of a curse. Nothing makes a presentation less engaging than piles of equations, tiny source code, and bullet points, but that’s precisely what Beamer makes easy to add.

I think some of the javascript libraries for presentations are a better fit as they make it easy to embed videos, animations and transitions that guide the eye to what matters. Unless you need to be able to send someone a pdf of the presentation, I’d hesitate to recommend using this library without large amounts of discipline.

1. 9

I think what’s going on here is that too many people have been sitting in university rooms listening to boring lecturers giving excruciating presentations made with Beamer and filled with hundreds of bullet points.

Not that I’m the biggest Beamer expert out there, but I use it for all my slides and I think the results are pretty good.

I think some of the javascript libraries for presentations are a better fit as they make it easy to embed videos, animations and transitions that guide the eye to what matters.

Animations, videos and transitions can be abused exactly like bullet points. In an effort to escape the boring-lecturer-effect, we should be careful not to err on the side of entertainment and produce presentations filled with animated gifs and almost zero content (I’ve seen many of those too, lately).

1. 2

I think some of the javascript libraries for presentations are a better fit as they make it easy to embed videos, animations and transitions that guide the eye to what matters.

Unless you want to print the slides..?

1. 1

Nothing makes a presentation less engaging than piles of equations, tiny source code, and bullet points, but that’s precisely what Beamer makes easy to add.

At university this has become quite popular. Instead of lecture notes we just have densely populated beamer presentations, which seem neither to read during a lecture nor to read when learning.

I think it’s a pity that many of the more interactive features of beamer beyond \pause are just forgotten, ignoring seemingly all principles of good presentation-making.

1. 1

I’m not clear even the advanced features really help. I think it matters what makes a tool easy to do.

1. 1

This is why I despise Beamer. Also it is a pain to use compared to alternatives.

2. 1

I totally agree! I have used reveal.js with pleasure and success, though I used only a bare minimum of the features, as I find most stuff in presentation software distractions not attractions.

1. 1

What javascript libraries do you have in mind? l’m a heavy (disciplined) Beamer user and, like @ema, think I produce quality slides, but I am curious about other tools for programatic presentation generation.

1. 1

Truthfully, these days I use reveal.js with Jupyter notebooks (https://github.com/damianavila/RISE)

I’ve used deck.js, reveal.js and eagle.js. Aside from needing to futz with npm these have all been perfectly adequate. Thanks to MathJax, I can still put in an equation if it’s needed. For some of them you can even use pandoc to generate the html directly from markdown https://pandoc.org/demos.html.

Like I said, if you are disciplined, Beamer can work really great. For me what counts is what the tools encourages you to do and not to do. From that standpoint, a lot of tools would have trouble outdoing sent

2. 1

That’s interesting to know. I’m in the process of converting my workshop slides from PowerPoint to beamer. Most of the slides are either code, short definitions, or diagrams, and I wanted to be able to easily find/replace my slides. They’re there to frame the live coding sections, so hopefully the plainness won’t be too much of a problem.

1. 1

I’ve been thinking of doing an Alloy webinar, so the information on recording and presentation is really helpful. Thank you!

1. 5

This was an interesting read. Thanks!

One thing, which would’ve been a cool addition, would’ve been a control graph of the system being analysed. There’s a lot of literature with examples of STPA/CAST-analyses for safety, but very few for security, and all of them are related to analysing a system around some physical process. Would’ve been interesting to see your take on it here. There’s a bit about extending STPA for Security e.g. here and here.

Another nice and a bit more practical resource for learning about STPA (The hazard analysis method based on STAMP) is the STPA Handbook (pdf) Leveson and Thomas published last year. Leveson’s 2012 book, at least for me, was at points a bit long winded (nonetheless a very good book), but I’ve found the handbook a better reference for analyses. It also covers a lot of typical common mistakes etc.

If I may nitpick a bit, STAMP is an accident model, STPA and CAST are analysis methods based on it :) Leveson extended on ideas from Jens Rasmussen, as she talks about e.g. in this publication. If you’re interested, check e.g. this influential paper from Rasmussen.

PS. The link to Leveson’s homepage at the end of the article is not working.

1. 1

Wow, that is a really good handbook. You should submit it as a lobsters link!

(I know I should include a control graph but I’m kinda procrastinating on making one :/)

1. 4

If you ever hear me say “I should use STAMP on something!” please punch me in the face. It’s for my own good.

1. 2

Nah, I’m gonna suggest 10 other things. Then, watch the mayhem. ;)

1. 3

There’s a bug in Match_NS: one of the selectors is on “Exits” instead of “Exists”. I like to leave the OTHER off case statements so that a lack of matching counts as an error.

1. 2

“Cosine Similarity tends to determine how similar two words or sentence are, It can be used for Sentiment Analysis, Text Comparison and being used by lot of popular packages out there like word2vec.”

Wouldn’t any distance metric do? As long as you choose the right vector space?

I was under the impression cosine similarity makes it easy to batch computation with highly tuned matrix multiplications

1. 4

Cosine similarity is not actually a metric and I think that is why people use it. Showing it is not a metric is easy because for metric spaces the only points that are zero distance away from another point are the points themselves. Cosine similarity in that sense fails to be a metric because for any given vector there are infinitely many vectors orthogonal to it and hence “zero” distance away. (But I just realized it’s even simpler than that because cosine similarity also gives negative values so it fails the positivity test as well.)

The relation to matrices that you mentioned are about positive definite bilinear forms and those give rise to dot products that are expressible as matrix multiplications and in vector spaces there is a way to define a metric based on dot products by defining the metric to be the dot product of the difference between two vectors with itself. Following through the logic the positive definite condition ends up being what is required to make this construction a metric.

1. 3

This is not really the problem. People convert cosine similarly into a pseudo distance by taking 1 - cos(u,v). This solves the problems that you mention.

The true problem is that the cosine is a non-linear function of the angle between two vectors, this violates the triangle inequality . Consider the vectors a and c with an angle of 90 degrees. Their cosine pseudo-distance is 1. Now add a vector b that has an angle of 45 degrees of both a and c. The cosine pseudo-distances between a and b, b and c are 0.29 rounded. So, the distance from a to c via b is shorter than the distance from a to c.

1. 2

Even with the pseudo-distance you still have the same problem with zero distances, as 1 - cos(u,v) is zero whenever the two points are tau radians apart.

1. 2

In most vector space models, these would be considered to be vectors with the same direction, so 0 would be the correct distance. Put differently, the maximum angle between two vectors is 180 degrees.

2. 1

Good point. I didn’t think about the triangle inequality failure.

3. 1

Thanks! Why would people want that (not actually being a metric)?

1. 1

The Wikipedia article has a good explanation I think. When working with tf-idf weights the vector coefficients are all positive so cosine similarity ends up being a good enough approximation of what you’d want out of an honest metric that is also easy to compute because it only involves dot products. But I’m no expert so take this with a grain of salt.

So I take back what I said about using it because it’s not a metric. I was thinking it has something to do with clustering by “direction” and there is some of that but it’s also pretty close to being a metric so it seems like a good compromise when trying to do matching and clustering types of work where the points can be embedded into some vector space.

4. 3

I was under the impression cosine similarity makes it easy to batch computation with highly tuned matrix multiplications

The same applies to Euclidean distance when computed with the law of cosines. Since the dot product is the cosine of the angle between two vectors, scaled by the vector magnitudes, the squared Euclidean distance between two points is:

|u|^2 + |v|^2 - 2u·v

(|u|^2 is the squared L2 norm of u, equations are a bit hard to do here)

Computing the euclidean distance in this way especially pays off when you have to compute the euclidean distance between a vector and a matrix or two matrices. Then the third term is a matrix multiplication UV, which as you say, is very well-optimized in BLAS libraries. The first two terms are negligible (lower order of complexity).

One of the reasons that cosine similarity is popular in information retrieval is that it is not sensitive to vector magnitudes. Vector magnitudes can vary quite a bit with most common metrics (term frequency, TF-IDF) because of varying document lengths.

Consider e.g. two documents A and B, where document B is document A repeated ten times. We would consider these documents to have exactly the same topic. With a term frequency or TF-IDF vector, the vectors of A and B would have the same direction, but different lengths. Since cosine similarity measures just the angle between the vectors, it correctly tell us that the documents have the same topic, whereas a metric such as Euclidean distance would indicate a large difference due to the different vector magnitudes. Of course, Euclidean distance could be made to work by normalizing document (and query) vectors to unit vectors.

I don’t want to bash this article too much, but it is not a very good or accurate description of the vector model of information retrieval. Interested readers are better served by e.g. the vector model chapter from Manning et al.:

https://nlp.stanford.edu/IR-book/pdf/06vect.pdf

1. 1

I must have been confusing the two

1. 8

A while back I decided to begrudgingly learn Erlang to better understand what all the fuss was about. This post convinced me that I’d have a lot more fun (and learn more!) learning elixir instead.

1. 4

Either one will serve you well, the tooling is a bit nicer with Elixir, the code is a lot more condensed with Erlang.

The “interesting” parts of Elixir, the macro system, is something best viewed with great suspicion–not coincidentally, it is also what clever folks naturally tend to gravitate towards. :(

1. 1

That’s a little funny, because almost the entirety of the Elixir syntax surface area is implemented in terms of macros :-)

1. 2

The main advantage of imperative code over functional is its performance. Being able to generate imperative from functional in certifiable way might negate a lot of advantages to coding in imperative style. You get the easy analysis and productivity of functional with efficiency of imperative.

That’s the dream anyway. I wonder how close this kind of work can get to it.

1. 3

I’d slightly qualify that sentence with “an advantage of imperative code over function is its control over constraints”. It might not be performance you’re looking for, but memory, low power usage, minimal latency, etc. Also, “control” could go either way. it can easily be the case that imperative code is worse for the constraint than the functional code. Quicksort is faster than Haskellsort, but Haskellsort is way faster than Bubblesort.

1. 1

That’s a great point. How to word it, though? Just “low-level control” or “control over low-level details of program execution?” I think I’ve seen the latter mentioned as a benefit of C language.

2. 2

I think the main trouble with imperative programming models is the problem of temporality and state explosion. The combinatorics completely overwhelm any analysis. The trouble with declarative models is somewhat the opposite, they hide too many details to get non-trivial results that are widely applicable. I think this tension is unavoidable so instead of trying to work around it better to embrace it and start with general purpose declarative models that are amenable to being refined into more imperative forms for optimization purposes.

1. 2

Yes, I agree with you on saving imperative for optimization step where possible. Far as combinatorics, I’ll add that there’s been excellent work in static/dynamic analysis focusing on interleavings with clever ways of bounding combinatorials to get past that for a lot of realistic examples. Always more of these turning up.

So, my default would be to design it high-level, synthesize an imperative implementation somehow, and apply those tools to it. If it passes, use imperative. If it fails, use non-imperative form. Runs in background or overnight to not slow developers down. Work like Lammichs and folks mixing Haskell with Rust also suggests a mix can happen where such tooling makes each piece (eg module) go imperative, tries analysis on each, and integrates only imperative versions that pass. So, as in Lammich’s piece, you get some benefits like speedups over purely functional or declarative code. And, in both these models, modifications still happen on non-imperative side so you keep maintenance benefits of non-imperative programming. What you think of this?

Oh yeah, I probably should add that I prefer all software to be efficient by default for the indirect benefits that can create. Adding it in case you’re wondering why I’d want an imperative optimization on something declarative that’s already “fast enough.” User might like having option of running their software on a cheaper box or using less electricity.

1. 2

What you think of this?

Completely missed the question so a bit late with an answer.

My current answer would be we don’t know how to deal with the state explosion problem for analyzing imperative implementations. I know that when Xavier and co. were working on CompCert they used a mixed strategy for register allocation which involved specifying and verifying as much as was possible with Coq and then leaving the harder parts to verifications during compile time

… CompCert uses Iterated Register Coalescing (IRC) [George and Appel 1996]. This algorithm is very effective, but it’s also quite complicated. In CompCert, this algorithm is not proven correct. Instead, after generating the graph, the compiler calls an OCaml implementation of IRC and then checks that the coloring is valid. If the checker confirms that the coloring is valid, the compiler uses it and proceeds along. If it does not confirm that it’s valid, compilation is aborted.

I think this is a fruitful approach that should be utilized more often where the verification of the hard parts can be staged in a verification pipeline and moved between stages as more pieces are proven correct. In general, I’m in favor of incorporating SAT/SMT solvers in the development pipeline and I’ve fruitfully used mixed-integer programs to solve allocation problems but this hits the same wall all other formal methods hit: general lack of knowledge and education about useful patterns that any software engineer can utilize.

Fundamentally it is a mindshare problem and it’s unclear to me how to effectively bridge the gap between current practices and “better” ways of building software systems. Mixing Rust and Haskell or another high-level declarative language seems to fit the pattern used in CompCert so in that sense there is definitely precedent.

1. 2

That technique is called translation validation created in 1998. The linked work is an example from Necula, who invented Proof-Carrying Code. It’s similar. They’re all part of an abstract pattern I call Untrusted Generator with Trusted Checker. That’s for anything: software, hardware, proof terms, whatever. In all instances, the setup allows us to know the untrusted part did its job so long as the smaller, simpler, trusted part works. Leroy did point out sometimes it’s easier to verify the generating part. So, we gotta go with easiest one on case by case basis.

“I’ve fruitfully used mixed-integer programs to solve allocation problems”

I’ll try to remember that. Mixed-integer is a technique I haven’t used before. Now I know it can do allocation. :)

“Fundamentally it is a mindshare problem and it’s unclear to me how to effectively bridge the gap between current practices and “better” ways of building software systems.”

I’ve been pushing for a gradual process that starts with Design by Contract. That link is good for project managers, too. ;) Essentially, you teach the benefits of contracts starting with simple stuff like ranges and ordering. Then, the contract-based, test generation plus runtime checks with fuzzers. Collect the data about how quickly one knocks out bugs with so little work. Also, the contract-based, test generation and fuzzing makes most unit tests unnecessary. They can focus on just what’s hard to express with contracts. Throw in some TLA+ for distributed stuff catching problems that take 35 steps to get to for illustrating model-checking superiority over testing in such examples. Maybe Cleanroom to illustrate engineered software. Then, these little things let the use and benefits of specs sink in with a percentage upgrading to stuff like Haskell or formal methods.

On formal methods side, I’ve been collecting data on what’s easiest to learn to teach the benefits. I have two methods that were specifically for education claiming to get results. The only problem each had was students needed a prior exposure to first-order logic and set theory to be comfortable with it. I found an easy resource on set theory to get them an intuition for it. I don’t have one on FOL. I’m up for any people have. Eventually, I’ll have a small chain of resources from the logic introduction to those courses or tools that can be tested for effectiveness on students. If that works, we tweak it to take them toward the heavier stuff. I also lean toward things like ASM’s and PlusCal since industrial experience shows people learned those more easily than stuff like Coq and HOL. ASM’s and B Method also support code generation.

So, those are the ideas I’ve been working with.

1. 1

Seems like a reasonable strategy.