bjz_

AFAIK, the flu vaccine doesn't prevent against all strains, because the virus mutates so rapidly year by year. They prepare it every year based on the worst/most common strains that were seen in opposite hemisphere's flu season. It does help limit the spread though, and is still really important to get.

I remember watching a talk where a formal methods researcher was talking about how, with the help of some grad students, they rebuilt one of Boeing's helicopter drone's flight control systems to use sel4 in a collaboration with DARPA. From memory the external security researchers could easily compromise the existing software, but failed to penetrate into the formally verified sel4 rewrite, even when they were given backdoor access to one of the subsystems as a helping hand. Every time they tried to escape the subsytem, seL4 would reboot them, leading the security researchers to say that it was the most secure flight control system they'd ever tested.

I'll see if I can dig it up - feel free to take it skeptically, I don't know how easy this experience was to reproduce. It was a pretty cool case study, however.

Edit:

This was the one! "Kathleen Fisher - From quadcopters to helicopters" https://www.youtube.com/watch?v=TH0tDGk19_c

Here's a mirror of an article from the ACM with more details: https://sudonull.com/post/3016

Records of the same structure but different names are equivalent. In fact tuples are just sugar over records with numeric fields starting from 1. Note that this is not the same as in OCaml, afaik.

> AFAIK SML is nominal

I guess I was referring to how records are structural. Although granted tagged unions are nominal, and you can get nominal typing through modules. I was probably wrong in posing it as 'one or the other' - seeing as many languages have a mix of both. I'm definitely not saying that nominal typing is bad, it's just that it's nice to have the option to go structural if you want, and many have not known that this option exists.

It's probably more that most mainstream typed languages, like C, C++, Java, C#, etc. have mainly gone down the nominal route, as opposed to languages like Standard ML and Typescript that tend to be more structural.

Structural vs. nominal typing is pretty well known in programming language design circles, but circulating that knowledge is a constant uphill challenge. One of the reasons many of us are frustrated with Go's designers were how quickly they threw this work under the bus as part of their initial marketing strategy, which kind of knocks away the ladder for anyone else who is curious to learn about this stuff.

Ahhh! Right! See, the context here is important. Continuations are pretty widely known and important in the context of programming language implementation and theory, which is why I was confused by your comment. In the context where this paper was presented (to programming language researchers), making the link between delimited continuations _would_ demystify a bunch, and could allow for transferring of knowledge and techniques between the fields.

> Continuations are well known to be completely mystifying.

Could you elaborate on what leads you to think this?

Yes! I did this many years ago, when it was all one course. I only got around to doing the SML part but it really improved how I approached learning new programming languages and frameworks (not just FP languages). I'm very thankful for what I learned, it has really help my a huge amount in my career! I'd highly recommend it to anyone who feels overwhelmed with all the 'new stuff' coming out. Much of it can be learned much easier if you look a little deeper and can ask the right questions.

Can't you be content with the fact that your work impacts and improves the lives of billions of people? What gives you the right to maintain a stranglehold over a market and drive off competition simply because you were lucky enough to be first to implement an idea, or had the fortune to have enough resources to stick it through the hard times?

Also note that companies are far from honest in this work - just look at what Google is doing to erode the web platform, and how it is leveraging it's search monopoly to drive businesses towards paying for ads.

I've felt this too. My best strategy is to do something productive with that natural stress and worry. Go to climate rallies. Move to banks that don't invest in fossil fuels. If you have retirement savings, make sure they are not used for fossil fuel investment (in Australia we have ethical super funds that commit to this). Call up you government representatives and make sure they know you are worried about the future and want them to act. Vote and donate to political candidates that support reducing emissions to zero at least by 2050. Get your friends and family to do the same. The biggest impact we can have is economic and political, and if we work together we can change a great deal!

Arson has always been around in Australia. But climate change exacerbates the impact. Less time for safely going hazard reduction burns, and drier forests, and less rain makes a big impact.

> At Google I remember a friend talking about how he cringed whenever he added more code to the pipeline that ingests the entire internet. He said that he wondered how much extra carbon was release into the atmosphere just because of his stupid code.

I wish companies were under more financial pressure to actually track and mitigate this. (hint hint, carbon taxes)

Trouble with "stage" is that is collides with the "stages" in "multistage programming" - so you're kind of adding to overloading in another field! It's also a field that has lots of applicability to the front-end space (eg. server-side rendering, Svelte, etc.)

Yeah! This was a big reason why we've invested in funding the work on https://github.com/n8willis/opentype-shaping-documents/ - hopefully this makes the barrier to entry to building font shaping engines a little lower for newcomers, and gives us a place to document findings, separate from any single implementation.

At the same level of performance though?

You might be interested in checking out https://typeclasses.com/. You have to subscribe, but they have some free content, including this nice section: https://typeclasses.com/phrasebook, which gets right into printing to the console, and working with state, multi-threading and mutation.

They're doing lots of great heavy lifting to get effects and handlers into a production language, and I don't think it's fair to write them off like this. Yes, it's hard, but they seem to be making positive progress.

Do you have to log in to access the link?

> The low runtime error rate is due to the amount of stuff that Racket manages to catch at compile time compared to other dynamic languages and to some fairly extensive automated testing.

Interested to know if typed racket was used for this, and if so, what the experience was like!

Yeah, I've be _really_ impressed with Lean's support. Wish other provers like Coq and Agda were at the same level (I know how challenging it is to do though).

Koka's docs are also okay, but could still do with some more work to help explain things in a compelling way: https://koka-lang.github.io/koka/doc/kokaspec.html

Interesting problem! So much of 'reconstructing bits of programs' is about satisfying the constraints of a fixed ascii representation of code. I am hoping that structured editing might be able to help with this, by allowing you to hide or show bits of code without relying on the type checker, but we need to have good ways of integrating with other tools for that to take off (like source control sites).

Yeah, type inference shouldn't really take a huge amount of time like that - for example Rust's type inference is a pretty small part of the overall compile time (although it can take longer if you do some crazy stuff with traits).

In Swift's case it seems like they've tried to add very flexible type inference (leaving off lots of stuff) to a very flexible type system (with inheritance, overloading, protocols, etc.). This is something that academics have been aware for decades causes problems with type checking performance. Similar problems have caused the designers of Scala 3 to go back to the drawing board to redesign the type system from the ground up, with a clearer formal semantics.

I do know that the Swift team are working really hard to make on demand editing/compiling better, but I don't know how far that work has come. Hopefully that improves things over time!

Nannou was recently bumped to 0.9 - they had a nice blog post here, with some neat examples (some commercial) including laser projection:

https://nannou.cc/posts/nannou_v0.9

Being a big Processing fan, and a bit of an artist too, this kind of creative framework is something I have been hoping was available way back when I started playing around with Rust in late 2012. Thanks goes to the Nannou team for all their hard work over the years in making this possible!

1. Rust _is_ helping Firefox development, and is a key part of why Firefox is remaining competitive. And they should have the flexibility to invest back into future R&D, and into supporting the open source projects that they depend on. That's part of what makes Mozilla so great as a company, and why many of us love it.

2. For the paid version that seems fine. But it seems fair that the free version of Firefox needs to be flexible in figuring out how to find sources of revenue. For example, if they pulled the plug on the predefined search engines then Mozilla would be dead pretty soon.

The lack of a type system in Elixir is a productivity killer though :(

So while we're at it we should look at breaking up Google as well.

Those can be integrated with dependent types too - for an example look at F*.

Yeah, I first saw this approach taken by the Rust announcements in the early days. It's a great demonstration of empathy to the reader!

Ah, that's very interesting! Yeah, perhaps Edwin Brady has been better at marketing it to a wider audience - which is not a bad thing at all.