Rolandt

BBC: The Tattooist of Auschwitz – and his secret love.

“For more than 50 years, Lale Sokolov lived with a secret – one born in the horrors of wartime Europe, in a place that witnessed some of the worst of man’s inhumanity to man.

It would not be shared until he was in his 80s, thousands of miles from that place.

Lale had been the Tattooist of Auschwitz.”

Link via MetaFilter.

Paul A. Kirschner, 3-Star Learning Experiences, Jan 12, 2018

Paul Kirschner's schtick is promoting the idea of compkete focus on learning with no distractions (which he believes cause extraneous cognitive load). Hence the reasoning behind this misplaced analogy: "Disrupting one’s own learning is an individual choice; harming the learning of other students in the class is disrespectful. Laptop distractions due to movement of images and laptop screen lighting and multitasking activities may cause involuntary shifts of attention among students in close proximity to laptop users." I'm thinking we should also ban loud clothing, shifting and fidgeting in your seats, air-conditioning turning off and on, windows, and clocks. Especially clocks.

Ben Lorica, O'Reilly, Jan 12, 2018

One thing that caught my eye here was the use of the word 'pedagogy' to refer to machine learning. I'm thinking they should maybe have used the term 'machinagogy' or 'aigogy' instead. Anyhow, most of these predictions are of the "current trends will continue" sort. But there are some good points about the need for improvements in hardware to improve AI, since it is so computationally intensive, and the use of automation "for creative pursuits like AI-generated music, images, and visual arts, which will also start appearing in commercial products." 

Donald Trump tweeted that he’s “like, really smart.” Anything in writing that uses “like” in this way sets off alarm bells, because it’s the ultimate weasel word. Here’s Trump’s series of tweets. Now that Russian collusion, after one year of intense study, has proven to be a total hoax on the American public, the Democrats … Continued

The post It’s, like, the ultimate weasel word. And it’s, like, really dumb to write it, President Trump. appeared first on without bullshit.

I’ve watched teenagers struggle with the most amazing things in high school and college. Their heads are crammed with Dickens and trigonometry but they can’t make a phone call or cook a meal. Nobody should graduate high school without knowing this stuff. So here are ten things we should teach in school and three things … Continued

The post Adulting 101: 10 things they really should teach teenagers at school — and 3 we could do with less of appeared first on without bullshit.

Over years of experience you begin to collect ways of working and talking about how you work that accrete into rules of thumb. Here are some that I reference pretty often. I’d love to hear others.

• One hour / day of analysis for every hour / day of research. 
  (I’m pretty sure that back in the early days it used to be 2:1 ratio but that was Before Agile. These days 1:1 is considered generous, but it is entirely necessary. If you don’t intend and allow time to do the analysis, don’t bother doing the research IMHO).  There are some thoughts on doing research analysis in agile teams that I mostly agree with here.
• The 70/30 rule
  Researchers should spend 70% of their time communicating, helping (and persuading) people to understand and act on the research and 30% of their time actually doing research. More on that here.
• The two week rule
  Don’t design anything for more than 2 weeks before you watch people using it. More on that here.
• More than three, less than ten
  Working out how many people to recruit can be tricky. It is much more important that you just get started doing research and keep doing it, than it is to tie yourself in knots working out sample size. That said, three people is almost always too few. For qualitative research, in the first instance, ten is very often more than you need. More on sample size here.
• One researcher per team
  Don’t spread researchers thinly across a bunch of teams. Researchers working across multiple teams tend not to be able to do the 70/3o rule and their research is less effective and impactful as a result. If you don’t have enough researchers to do this, prioritise your projects, let researchers do a good job for at least one team rather than a mediocre job for everyone. Also, you should read this as ‘at least one’ rather than ‘only one’. Some teams require multiple researchers. Avoid discussions about ratios of researchers : designers : devs whenever possible.

I’m aware some of these are a bit contentious, but they’ve worked for me. I’d love to hear any you’ve been using that work for you.

“Hold on — I need to check my Mentions.”

Ten years ago or more we had several blog-specific search engines and services: Technorati, BlogBridge, and others.

One of the great things about these services was not just being able to search for something but being able to set up persistent searches: that is, you’d get a search as an RSS feed, and in your feed reader you’d get results from all over the place on the thing you’re searching for.

In the obvious and common cases, you’d set up searches for people linking to your blog, writing about the apps you work on, mentioning the place where you work, and mentioning you.

I’d like to see something like this for today, but where the scope is just the Apple/Mac/iOS community. It would crawl the obvious sites (such as Daring Fireball and Loop Insight) and it would crawl the many blogs and microblogs that make up the community.

I think this is best as a web service, though it could have Mac and/or iOS client apps. It needs to provide feeds for people using feed readers.

* * *

With that reduced scope, and with the better tools and cheaper cloud computing these days, I don’t think it would be terribly expensive. Not like it was 15 years ago.

You might want to make money with this, though, and there are a few ways to do it: charge extra for things like notifications and email alerts. Charge money for client apps. Make the first three search feeds free, and charge money for a ten-pack of searches. Etc.

* * *

An alternate version of this idea isn’t a web service — it’s a Mac and/or iOS app that does the crawling. A kind of specialized Mac/iOS feed reader.

The list of feeds-to-crawl would probably just be an OPML file on the web, and the app would periodically grab that list.

(If you did this, you could use RSParser as starter code, since it parses OPML, RSS, Atom, JSON Feed, and RSS-in-JSON.)

This would make a great open source project, but it could just as well be free or for-pay.

* * *

One challenge is handling spam and abusive or hateful content. You’d most likely want to have a suggest-a-site form, so you don’t have to go out and find every single site there is.

But you have to be able to say no, and you have to be able to update the list of sites-to-crawl quickly if a site turns bad or inappropriate somehow.

You’d also need a way for users to report an issue.

(Again, the reduced scope — Apple-related blogs — makes this somewhat easier than if you tried to do the entire blogosphere.)

* * *

I want this! I’d use it every day. I know other people who would too.

But I’ve got enough on my plate that there’s no way I can do it myself — though I’d be happy to answer questions and provide feedback to anyone who does want to do it.

When I introduce myself as a data scientist, I often get questions like “What’s the difference between that and machine learning?” or “Does that mean you work on artificial intelligence?” I’ve responded enough times that my answer easily qualifies for my “rule of three”:

When you’ve written the same code 3 times, write a function

When you’ve given the same in-person advice 3 times, write a blog post

— David Robinson (@drob) November 9, 2017

The fields do have a great deal of overlap, and there’s enough hype around each of them that the choice can feel like a matter of marketing. But they’re not interchangeable: most professionals in these fields have an intuitive understanding of how particular work could be classified as data science, machine learning, or artificial intelligence, even if it’s difficult to put into words.

So in this post, I’m proposing an oversimplified definition of the difference between the three fields:

• Data science produces insights
• Machine learning produces predictions
• Artificial intelligence produces actions

To be clear, this isn’t a sufficient qualification: not everything that fits each definition is a part of that field. (A fortune teller makes predictions, but we’d never say that they’re doing machine learning!) These also aren’t a good way of determining someone’s role or job title (“Am I a data scientist?”), which is a matter of focus and experience. (This is true of any job description: I write as part of my job but I’m not a professional writer).

But I think this definition is a useful way to distinguish the three types of work, and to avoid sounding silly when you’re talking about it. It’s worth noting that I’m taking a descriptivist rather than a prescriptivist approach: I’m not interested in what these terms “should mean”, but rather how people in the field typically use them.

Data science produces insights

Data science is distinguished from the other two fields because its goal is an especially human one: to gain insight and understanding. Jeff Leek has an excellent definition of the types of insights that data science can achieve, including descriptive (“the average client has a 70% chance of renewing”) exploratory (“different salespeople have different rates of renewal”) and causal (“a randomized experiment shows that customers assigned to Alice are more likely to renew than those assigned to Bob”).

Again, not everything that produces insights qualifies as data science (the classic definition of data science is that it involves a combination of statistics, software engineering, and domain expertise). But we can use this definition to distinguish it from ML and AI. The main distinction is that in data science there’s always a human in the loop: someone is understanding the insight, seeing the figure, or benefitting from the conclusion. It would make no sense to say “Our chess-playing algorithm uses data science to choose its next move,” or “Google Maps uses data science to recommend driving directions”.

This definition of data science thus emphasizes:

• Statistical inference
• Data visualization
• Experiment design
• Domain knowledge
• Communication

Data scientists might use simple tools: they could report percentages and make line graphs based on SQL queries. They could also use very complex methods: they might work with distributed data stores to analyze trillions of records, develop cutting-edge statistical techniques, and build interactive visualizations. Whatever they use, the goal is to gain a better understanding of their data.

Machine learning produces predictions

I think of machine learning as the field of prediction: of “Given instance X with particular features, predict Y about it”. These predictions could be about the future (“predict whether this patient will go into sepsis”), but they also could be about qualities that aren’t immediately obvious to a computer (“predict whether this image has a bird in it”). Almost all Kaggle competitions qualify as machine learning problems: they offer some training data, and then see if competitors can make accurate predictions about new examples.

There’s plenty of overlap between data science and machine learning. For example, logistic regression can be used to draw insights about relationships (“the richer a user is the more likely they’ll buy our product, so we should change our marketing strategy”) and to make predictions (“this user has a 53% chance of buying our product, so we should suggest it to them”).

Models like random forests have slightly less interpretability and are more likely to fit the “machine learning” description, and methods such as deep learning are notoriously challenging to explain. This could get in the way if your goal is to extract insights rather than make predictions. We could thus imagine a “spectrum” of data science and machine learning, with more interpretable models leaning towards the data science side and more “black box” models on the machine learning side.

Most practitioners will switch back and forth between the two tasks very comfortably. I use both machine learning and data science in my work: I might fit a model on Stack Overflow traffic data to determine which users are likely to be looking for a job (machine learning), but then construct summaries and visualizations that examine why the model works (data science). This is an important way to discover flaws in your model, and to combat algorithmic bias. This is one reason that data scientists are often responsible for developing machine learning components of a product.

Artificial intelligence produces actions

Artificial intelligence is by far the oldest and the most widely recognized of these three designations, and as a result it’s the most challenging to define. The term is surrounded by a great deal of hype, thanks to researchers, journalists, and startups who are looking for money or attention.

When you’re fundraising, it’s AI
When you’re hiring, it’s ML
When you’re implementing, it’s linear regression
When you’re debugging, it’s printf()

— Baron Schwartz (@xaprb) November 15, 2017

This has led to a backlash that strikes me as unfortunate, since it means some work that probably should be called AI isn’t described as such. Some researchers have even complained about the AI effect: “AI is whatever we can’t do yet”.¹ So what work can we fairly describe as AI?

One common thread in definitions of “artificial intelligence” is that an autonomous agent executes or recommends actions (e.g. Poole, Mackworth and Goebel 1998, Russell and Norvig 2003). Some systems I think should described as AI include:

• Game-playing algorithms (Deep Blue, AlphaGo)
• Robotics and control theory (motion planning, walking a bipedal robot)
• Optimization (Google Maps choosing a route)
• Natural language processing (bots²)
• Reinforcement learning

Again, we can see a lot of overlap with the other fields. Deep learning is particuarly interesting for straddling the fields of ML and AI. The typical use case is training on data and then producing predictions, but it has shown enormous success in game-playing algorithms like AlphaGo. (This is in contrast to earlier game-playing systems, like Deep Blue, which focused more on exploring and optimizing the future solution space).

But there are also distinctions. If I analyze some sales data and discover that clients from particular industries renew more than others (extracting an insight), the output is some numbers and graphs, not a particular action. (Executives might use those conclusions to change our sales strategy, but that action isn’t autonomous) This means I’d describe my work as data science: it would be cringeworthy to say that I’m “using AI to improve our sales.”

please

please

please do not write that someone who trained an algorithm has "harnessed the power of AI"

— Dave Gershgorn (@davegershgorn) September 18, 2017

The difference between artificial intelligence and machine learning is a bit more subtle, and historically ML has often been considered a subfield of AI (computer vision in particular was a classic AI problem). But I think the ML field has largely “broken off” from AI, partly because of the backlash described above: most people who to work on problems of prediction don’t like to describe themselves as AI researchers. (It helped that many important ML breakthroughs came from statistics, which had less of a presence in the rest of the AI field). This means that if you can describe a problem as “predict X from Y,” I’d recommend avoiding the term AI completely.

by today's definition, y=mx+b is an artificial intelligence bot that can tell you where a line is going

— Amy Hoy ✨ (@amyhoy) March 29, 2017

Case study: how would the three be used together?

Suppose we were building a self-driving car, and were working on the specific problem of stopping at stop signs. We would need skills drawn from all three of these fields.

• Machine learning: The car has to recognize a stop sign using its cameras. We construct a dataset of millions of photos of streetside objects, and train an algorithm to predict which have stop signs in them.

• Artificial intelligence: Once our car can recognize stop signs, it needs to decide when to take the action of applying the brakes. It’s dangerous to apply them too early or too late, and we need it to handle varying road conditions (for example, to recognize on a slippery road that it’s not slowing down quickly enough), which is a problem of control theory.

• Data science: In street tests we find that the car’s performance isn’t good enough, with some false negatives in which it drives right by a stop sign. After analyzing the street test data, we gain the insight that the rate of false negatives depends on the time of day: it’s more likely to miss a stop sign before sunrise or after sunset. We realize that most of our training data included only objects in full daylight, so we construct a better dataset including nighttime images and go back to the machine learning step.

I struggled for a long time when the nice folks at the Heat Rocks podcast asked me which Prince album I'd want to talk about on their show. Oliver Wang and Morgan Rhodes run an amazing podcast, where every episode is a deep-dive into a classic album.

Ultimately, because of its significance and relative lack of prominence amongst casual fans, I settled on Prince's 1982 classic, 1999. In the finished show, we talk about everything from how Quincy Jones and Michael Jackson were influenced by the sound of 1999 to my own personal revelations about faith, as inspired by discovering that Prince didn't actually write the Lord's Prayer.

If you ain't busy for the next 45 minutes, please do check out this wonderful conversation!

A few months ago, I got the wonderful opportunity to talk to Barry Ritholtz, who's best known as a Bloomberg View columnist and for his excellent "Masters in Business" podcast, but whom I've known online for many years.

We talked about a topic that's incredibly important to me, the ethical challenges facing all of us who create technology. It's a wide-ranging conversation that's over an hour long, but I hope you'll take the time to listen, as this is a discussion we all need to be engaging in.

There's also a longer story in the BloombergView site covering a bit of what we discussed.

I've been reading the book Building High Integrity Applications with Spark to learn more about the [SPARK/Ada](https://en.wikipedia.org/wiki/SPARK_(programming_language)) language for formal verification. It's a great book that goes through lots of examples of how to do proofs in Spark. I wrote a post on Spark/Ada earlier this year and tried some of the examples in the GNAT edition.

While working through the book I oftened compared how I'd implement similar examples in ATS. I'll go through one small example in this post and show how the dependent types of ATS allow capturing the invariants of a function and check them at type checking time to prove the absence of a particular class of runtime errors.

The example I'm looking at from the book is from the Loop Invariants section, which aims to prove things about iterative loops in Ada. The procedure Copy_Into copies characters from a String into a Buffer object that has a maximum capacity. If the source string is too short then the buffer is padded with spaces. The Spark/Ada code from the book is:

procedure Copy_Into(Buffer: out Buffer_Type; Source: in String) is
  Characters_To_Copy : Buffer_Count_type := Maximum_Buffer_Size;
begin
  Buffer := (others => ' ');
  if Source'Length < Characters_To_Copy then
    Characters_To_Copy := Source`Length;
  end if;
  for Index in Buffer_Count_Type range 1 .. Characters_To_Copy loop
    pragma Loop_Invariant (Characters_To_Copy <= Source'Length and
                           Characters_To_Copy = Characters_To_Copy'Loop_Entry);
    Buffer(Index) := Source(Source'First + (Index - 1));
  end loop;
end Copy_Into;

This is quite readable for anyone familiar with imperative languages. The number of characters to copy is initially set to the maximum buffer size, then changed to the length of the string if it is less than that. The buffer is set to contain the initial characters ' '. The buffer is 1-indexed and during the loop the characters from the string are copied to it.

The Loop_Invariant pragma is a Spark statement that tells the checker that certain invariants should be true. The invariant used here is that the number of characters to copy is always less than or equal to the length of the string and does not change within the loop. Given this loop invariant Spark can assert that the indexing into the Source string cannot exceed the bounds of the string. Spark is able to reason itself that Buffer does not get indexed out of bounds as the loop ranges up to Characters_To_Copy which is capped at Maximum_Buffer_Size. I'm not sure why this doesn't need a loop invariant but the book notes that the Spark tools improve over time at what invariants they can compute automatically. As an example, the second invariant check above for Characters_To_Copy'Loop_Entry isn't needed for newer versions of Spark but is kept to enable checking on older toolchains.

For ATS I modeled the Buffer type as an array of characters:

stadef s_max_buffer_size: int = 128
typedef Buffer0 = @[char?][s_max_buffer_size]
typedef Buffer1 = @[char][s_max_buffer_size]
val max_buffer_size: size_t s_max_buffer_size = i2sz(128)

In ATS, @[char][128] represents an array of contiguous 'char' types in memory, where those char's are initialized to value. The @[char?][128] represents an array of unitialized char's. It would be a type error to use an element of that array before initializing it. The '0' and '1' suffixes to the 'Buffer' name is an ATS idiom for uninitialized and initialized data respectively.

The stadef keyword creates a constant in the 'statics' system of ATS. That is a constant in the language of types, vs a constant in the language of values where runtime level programming is done. For this post I have prefixed variables in the 'statics' system with s_ to make it clearer where they can be used.

The max_buffer_size creates a constant in the 'dynamics' part of ATS, in the language of values, of type "size_t max_buffer_size". size_t is the type for indexes into arrays and size_t 128 is a dependent type representing a type where only a single value matches the type - 128 in this instance. The i2sz function converts an integer to a size_t. So in this case we've created a max_buffer_size constant that can only ever be the same value as the s_max_buffer_size type level constant.

The ATS equivalent of copy_into looks like:

fun copy_into {n:nat}
       (buffer: &Buffer0 >> Buffer1, source: string n): void = let
  val () = array_initize_elt(buffer, max_buffer_size, ' ')
  val len = string1_length(source)
  stadef s_tocopy = min(s_max_buffer_size, n)
  val tocopy: size_t s_tocopy = min(max_buffer_size, len)
  fun loop {m:nat | m < s_tocopy } .<s_tocopy - m>.
        (buffer: &Buffer1, m: size_t m): void = let
    val () = buffer[m] := source[m]
  in
    if m < tocopy - 1 then loop(buffer, m+1)
  end
in
  if len > 0 then
    loop(buffer, i2sz(0))
end 

Starting with the function declaration:

fun copy_into {n:nat}
       (buffer: &Buffer0 >> Buffer1, source: string n): void

The items between the curly brackets, {...}, are universal variables used for setting constraints on the function arguments. Between the round brackets, (...), are the function arguments. The return type is void. The function takes two arguments, buffer and source.

The buffer is a reference type, represented by the & in the type. This is similar to a reference argument in C++ or a pointer argument in C. It allows modification of the argument by the function. The Buffer0 >> Buffer1 means on entry to the function the type is Buffer0, the uninitialized char array described earlier, and on exit it will be a Buffer1, an initialized char array. if the body of the function fails to initialize the elements of the array it will be a type error.

The source argument is a string n, where n is a type index for the length of the string. By using a dependently typed string here we can use it later in the function body to set some invariants.

In the body of the function the call to array_initize_elt sets each element of the array to the space character. This also has the effect of changing the type stored in the array from char? to char, and the array is now a valid Buffer1. This matches the type change specified in the function declaration for the buffer argument.

The next three lines compute the number of characters to copy:

val len = string1_length(source)
stadef s_tocopy = min(s_max_buffer_size, n)
val tocopy: size_t s_tocopy = min(max_buffer_size, len)

The length of the string is obtained. The string1_ prefix to function names is an idiom to show that they operate on dependently typed strings. string1_length will return the string length. It returns a dependently typed size_t x, where x is the length of the string. This means that calling string_length not only returns the length of the string but it sets a constraint such that the type index of the result is equal to the type index of the string passed in. Here is the declaration of string1_length from the prelude (with some additional annotations removed):

fun string1_length {n:int} (x: string n): size_t n

The reuse of the n in the argument and result type is what tells the compiler to set the constraint when it is called. This is important for the next two lines. These perform the same operation, once in the statics and once in the dynamics. That is, once at the type level and once at the runtime level. The stadef sets a type level constant called s_tocopy to be constrained to be the same as the minimum of the max buffer size and the type level string length, n. The val line sets the runtime variable to the same calculation but using the runtime length. These two lengths must much as a result of the call to string1_length described earlier. The type of tocopy ensures this by saying that it is the singleton type that can only be fulfilled by the value represented by s_tocopy.

ATS has looping constructs but it's idiomatic to use tail recursion instead of loops. It is also easier to create types for tail recursive functions than to type iterative loops in ATS. For this reason I've converted the loop to a tail recursive function. When ATS compiles to C it converts tail recursive functions to a C loop so there is no danger of stack overflow. The looping function without dependent type annotations would be:

fun loop (buffer: &Buffer1, m: size_t): void = let
  val () = buffer[m] := source[m]
in
  if m < tocopy - 1 then loop(buffer, m+1)
end

It takes a buffer and an index, m, as arguments and assigns to buffer at that index the equivalent entry from the source string. If it hasn't yet copied the number of characters needed to copy it tail recursively calls itself, increasing the index. The initial call is:

loop(buffer, i2sz(0))

i2sz is needed to convert the integer number zero from an int type to a size_t type.

The declaration for the loop function contains the dependent type definitions that give invariants similar to the Spark example:

fun loop {m:nat | m < s_tocopy } .<s_tocopy - m>.
      (buffer: &Buffer1, m: size_t m): void = let

Starting with the arguments, the buffer is a Buffer meaning it must be an initialized array. The index, m is a dependently typed size_t m where m at the type level is constrained to be less than the number of characters to copy. This ensures that the indexing into the buffer and source string is never out of bounds due to the previous statements that set s_tocopy to be the lesser of the maximum buffer size and the string size. s_tocopy is needed here instead of tocopy due to universal arguments being written in the language of the typesystem, not the runtime system.

The body of the loop does the copying of the indexed character from the source string to the buffer and recursively calls itself with an incremented index if it hasn't copied the required number of characters.

  val () = buffer[m] := source[m]
in
  if m < tocopy - 1 then loop(buffer, m+1)

Due to the constraints set in the function declaration the buffer and source string indexes are checked at compile time to ensure they aren't out of bounds, and the recursive call to loop will fail typechecking if an out of bounds index is passed as an argument.

One issue with recursive functions is that they could loop forever if the termination condition check is incorrect, or the variables being used in that check don't explicitly increase or decrease. In this case the index must increase to eventually reach the value for the termination check.

ATS resolves this by allowing termination metrics to be added to the function. This is the part of the function declaration that is bracketed by .< ... >. markers. The expression inside these markers is expected to be in the 'statics' constraint language and evaluate to a tuple of natural numbers that the compiler needs to prove are lexicographically decreasing in value. The loop index counts up so this needs to be converted to a decreasing value:

.<s_tocopy - m>.

This is done by taking the static constant of the number of characters to copy and subtracting the index value. The compiler proves that each recursive call in the body of the function results in something strictly less than the previous call. With the termination metric added it statically proves that the recursive function terminates.

The program can be run and tested with:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

stadef s_max_buffer_size: int = 128
typedef Buffer0 = @[char?][s_max_buffer_size]
typedef Buffer1 = @[char][s_max_buffer_size]
val max_buffer_size: size_t s_max_buffer_size = i2sz(128)

fun copy_into {n:nat}
    (buffer: &Buffer0 >> Buffer1, source: string n): void = let
  val () = array_initize_elt(buffer, max_buffer_size, ' ')
  val len = string1_length(source)
  stadef s_tocopy = min(s_max_buffer_size, n)
  val tocopy: size_t s_tocopy = min(max_buffer_size, len)
  fun loop {m:nat | m < s_tocopy } .<s_tocopy - m>.
        (buffer: &Buffer1, m: size_t m): void = let
    val () = buffer[m] := source[m]
  in
    if m < tocopy - 1  then loop(buffer, m+1)
  end
in
  if len > 0 then
    loop(buffer, i2sz(0))
end 

implement main0() = let
  var  b = @[char?][max_buffer_size]()
  val () = copy_into(b, "hello world")
  fun print_buffer {n:nat | n < s_max_buffer_size}
                   .<s_max_buffer_size - n>.
       (buffer: &Buffer1, n: size_t n):void = let
    val () = if n = 0 then print!("[")
    val () = print!(buffer[n])
    val () = if n = max_buffer_size - 1 then print!("]")
  in
    if n < 127 then print_buffer(buffer, n + 1)
  end
  val () = print_buffer(b, i2sz(0))
in
  ()
end

This example creates the array as a stack allocated object in the line:

var  b = @[char?][max_buffer_size]()

Being stack allocated the memory will be deallocated on exit of the scope it was defined in. It's also possible to create a heap allocated buffer and pass that to copy_into:

implement main0() = let
  val (pf_b , pf_gc| b) = array_ptr_alloc<char>(max_buffer_size)
  val () = copy_into(!b, "hello world")
  fun print_buffer {n:nat | n < 128} .<128 - n>. (buffer: &(@[char][128]), n: int n):void = let
    val () = if n = 0 then print!("[")
    val () = print!(buffer[n])
    val () = if n = 127 then print!("]")
  in
    if n < 127 then print_buffer(buffer, n + 1)
  end
  val () = print_buffer(!b, 0)
  val () = array_ptr_free(pf_b, pf_gc | b)
in
  ()
end

This explicitly allocates the memory for the array using array_ptr_alloc and dereferences it in the copy_into call using the '!b' syntax. Note that this array is later free'd using array_ptr_free. Not calling that to free the memory would be a compile error.

Although this is a simple function it demonstrates a number of safety features:

• The destination buffer cannot indexed beyond its bounds.
• The source string cannot be indexed beyond its bounds.
• There can be no buffer overflow on writing to the destination buffer.
• There can be no uninitialized data in the buffer on function exit.
• The internal recursive call must terminate.

The book Building High Integrity Applications with Spark is a great book for learning Spark and also for learning about the sorts of proofs used in production applications using Spark/Ada. Apart from learning a bit about Spark it's also a good exercise to think about how similar safety checks can be implemented in your language of choice.

Alan Blinder and Michael Wines reporting for The New York Times:

A panel of federal judges struck down North Carolina’s congressional map on Tuesday, condemning it as unconstitutional because Republicans had drawn the map seeking a political advantage.

The ruling was the first time that a federal court had blocked a congressional map because of a partisan gerrymander, and it instantly endangered Republican seats in the coming elections.

Go math.

Tags: gerrymandering

Nathan Gitter:

I noticed an unusual behavior of the iPhone X home indicator while working on my most recent app. The app’s background near the home indicator is purple. When the app launches, the home indicator is very light gray.

But something odd happened when I pressed the app’s “share” button, which opened a default iOS activity view (aka “share sheet”). When I hit the “cancel” button to close the activity view, the home indicator animated to a dark gray color.

Home indicator starts light, then a share sheet passing makes it dark.

Even though the background color was exactly the same, the light-colored activity view passing underneath caused the home indicator to change color. The only way to get the home indicator back to its original color was to leave the app and come back.

I had never seen this before, and it prompted my curiosity.

Fascinating study of the iPhone X's Home indicator behavior. I had no idea that the indicator adapted to background color changes within the bar itself. Don't miss the second (and more technical) half of the story with Gitter's detailed color tests.

→ Source: medium.freecodecamp.org

There are a seemingly endless number of ways to represent colors. Whether you’re a professional designer or developer, or someone who just wants to update a website template, you’ve undoubtedly come across several. The trouble with so many different formats is that it guarantees that at some point, the color value you have won’t be the one you require. Aquarelo is a beautifully-designed new Mac app that cuts through the thicket of formats to help you find the colors you want and convert them to the format you need.

Many of the color utilities I’ve used in the past on the Mac and iOS have been abandoned, so it was good to see a new one released that’s as polished as Aquarelo. The main UI resembles a swatch of colors with a couple of additional controls. There are two text fields for entering color information and a stepper control in the center of the window for indicating how many colors you want to create.

Type an RGB or HEX value or color name into each text field, and Aquarelo generates a range of colors between the two you entered. You can even drag a color into the app from the system color picker. One small quibble I have with dragging colors into Aquarelo is that you can only drag them onto the text fields in the app. I think it would feel more natural to drop colors onto the endpoint colors in instead.

Aquarelo supports many formats.

I particularly like that Aquarelo allows for adding colors by name using terms like ‘neon green,’ ‘dark brown,’ or ‘pale pink.’ It’s a delightful touch that feels a little magical and simultaneously removes the friction of getting started for anyone who isn’t a color expert. It would be nice, however, to be able to adjust endpoint colors with a color wheel or some other mechanism when the color described isn’t quite what I intended.

Another area in which Aquarelo shines is exporting color values. At the top of the center of the window, you can pick one of 36 export formats. Clicking on any of the colors in your swatch copies the color in that format to the clipboard for pasting wherever you need it. There’s also a button for exporting the entire swatch of colors in one of 11 different formats.

An individual color card.

The variety of export options is impressive. For example, you can export a series of colors as Swift or Objective-C, and Aquarelo generates the code files for you for dropping into an Xcode project. There’s also a URL scheme for adding colors to Aquarelo. With the app installed, you can use URLs with HEX values like these to set the endpoint colors of a series:

aquarelo://last/#ef00cc
aquarelo://first/#00ffff

Additional options are available by right-clicking on a color. Picking ‘color details’ from the contextual menu opens a card for that color that includes its name, HEX and RGB values, an export button, and buttons to send the color to Adobe’s Photoshop and Illustrator apps. A Sketch plugin and a PopClip extension that let you send HEX values to Aquarelo from those apps are available on the Aquarelo website as separate downloads.

Aquarelo's contextual Touch Bar support.

Aquarelo supports the Touch Bar too. With a series of colors displayed, you can tap a color on the Touch Bar to copy its value to the clipboard. If a single color window is open, the Touch Bar’s colors are replaced with shortcuts to copy the RGB or HEX values, send the values to Photoshop or Illustrator, or export the color value in another format.

There are a couple of features I’d like to see added to Aquarelo to round it out. The first is the ability to save color swatches. You can export a series of colors as HTML, which creates a web page of your colors that will open them in Aquarelo with a click. However, I’d also like to be able to save a swatch with a name and drop it in a folder with other project files, so I can just open it up again in Aquarelo without recreating it from an HTML file.

Colors can be exported as HTML.

I would also like to see Aquarelo integrated with the system share sheet so I can quickly send a color swatch to someone as an image. The existing export options are excellent, but sometimes a simple image file sent in Messages is all I need to get someone’s thoughts on a color scheme.

If you work with colors, Aquarelo is an excellent addition to your set of tools. The wide array of export options make it a good choice for developers and designers and provides flexibility for sharing color choices with colleagues in whatever format they prefer. There are a couple of features I’d like to see added to Aquarelo, but none are deal-breakers. I look forward to seeing where developer Giovanni Cusaro takes the app next.

Aquarelo is available on the Mac App Store.

Support MacStories Directly

Club MacStories offers exclusive access to extra MacStories content, delivered every week; it's also a way to support us directly.

Club MacStories will help you discover the best apps for your devices and get the most out of your iPhone, iPad, and Mac. Plus, it's made in Italy.

We are entering the era of intelligent things where smart devices seep into every aspect of our lives. As AI continues to evolve and IoT devices proliferate, the two transformative technologies converge, forming something called AIoT (the artificial intelligence of things) or some may refer to it as the next generation of IoT. Sounds a […]

How a Taiwan-based AIoT startup is taking on the next big wave originally appeared on TechNode

Daniel Terdiman, Fast Company, Jan 13, 2018

According to this article, "Google and Lenovo pulled back the wraps on their entrant into the stand-alone VR world, the Mirage Solo, a device that has all its computing onboard, and which is capable of positional tracking with no external sensors." These aren't available commercially yet, but it won't be long. Meanwhile, "HTC said it was focusing its stand-alone work on a device called the Vive Focus, which it plans on selling only in China."

Nick Summers, Engadget, Jan 13, 2018

This is a fascinating set of photos from a display at the Consumer Electronics Show (CES) in Las Vegas. Normally the computer would have a case, but here we can see the coils and coolant arrangements needed to keep this 50 quantum bit (qubit) computer functioning. The system cools from top to bottom, down to 10 millionths of a degree above absolute zero. 

Brent Simmons asks

Ten years ago or more we had several blog-specific search engines and services: Technorati, BlogBridge, and others.

One of the great things about these services was not just being able to search for something but being able to set up persistent searches: that is, you’d get a search as an RSS feed, and in your feed reader you’d get results from all over the place on the thing you’re searching for.

In the obvious and common cases, you’d set up searches for people linking to your blog, writing about the apps you work on, mentioning the place where you work, and mentioning you.

Doesn’t Superfeedr fit that bill today?

Also, I miss referer logs.

Last night on Twitter, I noted that the company's iOS app now appends a query parameter based on an app's bundle identifier when you share a tweet's link via the system share sheet.

As some have noted, this appears to be a recent change in Twitter for iOS, which is less than ideal as the resulting link contains a long string of URL-encoded garbage. More than ugly URLs, however, what bothered me was Twitter's implicit tracking of which apps users invoke to share links with – something that even applies to core iOS features such as Apple's own Messages extension.

I wondered whether Apple should consider this a violation of App Store guidelines, but it appears that Twitter isn't breaking any rules by appending app-based query parameters to their shareable URLs. Benjamin Mayo looked into this feature and explained how Twitter is leveraging public iOS APIs to read bundle identifiers from the share sheet – he even posted a proof-of-concept code snippet to show how it'd work in practice.

He writes:

In reality, this is very easily achieved. As part of the activity provider API, the system asks for content to share for each sharing extension the user has installed. The Apple framework openly passes the activity type to the app. Twitter simply takes the base URL it wants to share and appends the ‘garbage’ before returning.

And:

The important thing to note here is that the mechanism is innocuous and uses valid APIs provided by Apple. Twitter is not exploiting private APIs to achieve this. A cursory look at the app review guidelines suggests to me there are no grounds for Apple to scold Twitter (or any other app) for doing it.

My personal stance is that this is annoying but does not violate user privacy. Importantly, Twitter cannot append arbitrary information to its URLs system-wide; it is confined to cases where users share something from inside the Twitter app itself. I don’t really see a justification for Apple to amend the guidelines to disallow it. I just take it as another reason not to use the official Twitter app.

In conclusion, if links to tweets you copied from the Twitter app suddenly look longer and messier than before, this is why. Personally, while Twitter may be taking advantage of a publicly available API, I still think the implementation is, at the very least, in poor taste – especially because it's coming from the same company that used to scan users' devices to list installed apps and deliver "tailored content" based on them. Even though I won't stop using the Twitter app because of this, I wish Twitter would revert to standard, clean URLs when sharing tweets from the app. I also hope Apple is taking a closer look at this.

→ Source: benjaminmayo.co.uk

Alex Hern, reporting for The Guardian on the results of Safari's new Intelligent Tracking Prevention (ITP), launched last year with iOS 11 and macOS High Sierra (via John Gruber):

Internet advertising firms are losing hundreds of millions of dollars following the introduction of a new privacy feature from Apple that prevents users from being tracked around the web.

Advertising technology firm Criteo, one of the largest in the industry, says that the Intelligent Tracking Prevention (ITP) feature for Safari, which holds 15% of the global browser market, is likely to cut its 2018 revenue by more than a fifth compared to projections made before ITP was announced.

Here's how Apple officially describes ITP in Safari 11's documentation:

Added Intelligent Tracking Prevention, which updates the default cookie and website data policy to isolate and remove cookies and website data for sites with the ability to track users across-site.

This isn't the first time ad companies have complained about Apple's protection of user privacy in Safari and stance against invasive cross-site tracking. In September, six trade groups claimed Apple was "sabotaging" the industry with a "unilateral and heavy-handed approach", to which Apple responded:

“Ad tracking technology has become so pervasive that it is possible for ad tracking companies to recreate the majority of a person’s web browsing history,” according to an Apple spokesperson. “This information is collected without permission and is used for ad re-targeting, which is how ads follow people around the Internet.”

"Unilateral" is exactly right: Apple should only care for the interests of users buying their devices, not those of third-party ad companies creepily tracking them around the web.

Cross-site tracking and ad targeting has gotten so out of hand over the past couple of years, it's become a regular comment from friends who don't follow tech news – "Why am I seeing an ad for something I was checking out two days ago on another site?" is a question I hear frequently despite the existence of third-party ad blockers and Apple's own ITP in Safari. Personally, I think the more Apple can advance ITP, the better it is for the privacy of all iOS users.

→ Source: theguardian.com

Limited Edition Bronze KEYone (Photo BlackBerry Mobile)

Official statement from BlackBerry Mobile/TCL:

Why is Europe experiencing a three months delay in security updates?

We are 100% committed to our security updates, and while we are aware there’s been a delay in security updates for certain consumers in Europe recently, we are working with our partners to fix these issues quickly and ensure the January update is rolled out soon.

As always I would like to hear what actually makes them fail so hard.

Update 2018-01-12: After three months KEYone got its update. Now on 7.1.1 05-Jan-2018.

Homekit ist eine feine Sache. Sind die Geräte erst einmal konfiguriert, lassen sie sich einfach in der Home App bedienen, sie lassen sich automatisieren und man kann sie per Siri steuern. Manchmal will man aber einfach einen Knopf drücken. Und genau das löst Eve Button. Ich habe ihn in der Home App als neues Accessory hinzugefügt und dann bestimmt, was passiert, wenn man den Knopf drückt. Das hat auf Anbieb funktioniert, ohne jede Installation von Software. Eve Button versteht drei verschiedene Aktionen: einfach drücken, doppelt drücken oder lange halten. Damit kann er drei verschiedene Befehlsketten anstoßen.

Von der Funktion her gleicht der Eve Button dem Logitech POP, von dem ich bereits zwei einsetze. POP ist vielseitiger aber auch komplizierter. Er braucht eine Bridge, die in Homekit aufgenommen wird. Die steckt irgendwo in einer Steckdose und brückt zwischen Buttons und dem WLAN. In der POP App legt man dann fest, welche POP zu Homekit gehört und welcher unabhängig bleiben soll, etwa um Sonos zu schalten. Bei Eve Button entfällt die Bridge. Er redet direkt mit dem Apple TV, das als Homekit Hub fungiert.

Wie der POP ist auch Eve Button batteriegetrieben. Die CR2032 wird wahrscheinlich "ewig" halten, denn die Funkverbindung geht über Bluetooth LE. Der Alurahmen ist formschön und fasst sich gut an. Will man den Button auf eine empfindliche Oberfläche legen, dann klebt man vier winzige mitgelieferte Füßchen darunter. Bei mir liegt er einfach lose auf dem Tisch rum.

Ich wollte eigentlich noch ein bisschen warten, bis ich ein Urteil darüber fälle, zumal es den Button erst nächste Woche zu kaufen gibt. Aber so simpel wie das Teil ist, habe ich es sofort adoptiert. Editor-refuses-to-give-it-back award.

Change of management at IBM for the collaboration business. Inhi Cho Suh moves on as GM Watson Customer Engagement. Bob Schultz is the new GM Watson Talent and Collaboration Solutions, which you can read as Kenexa + Lotus. Bob comes from the ´Kenexa side of the business and was hired by IBM when John Hernandez left. Bob is not a career IBMer but was previously working at Citrix VMware and HPQ. I am hearing only good things about him.

Wenn man eine Siri am Handgelenk hat, muss man nicht durch's Zimmer rufen. Außerdem kennt die schon alle HomeKit-Szenen.

I bought Sinéad O’Connor’s debut, The Lion and the Cobra, because Mandinko was on the radio and I liked it. The first time I played it, not having looked at the track listing, I noticed some meditative crooning about “Dublin in a Rainstorm”; the next time, a gut-grabbing throaty chant: “You should have left the lights on”; and then another time a howling declaration about rising, a phoenix from the flame. It took me a while to notice that all of these were from the same track: Troy. It’s a hell of a song.

It’s a hell of an album too; other highlights are Never Get Old and A Drink Before the War, which inspired me to a grief-stricken piece on the eve of the Iraq war. O’Connor recorded and produced on her own, twenty years old and seven months pregnant, on the way out of an abusive family. It’s an explosion of talent, songwriting and singing and arranging.

The word “Troy”, and the lyric about burning it, are a borrow from Yeats’ No Second Troy, which I hadn’t known until I chanced across the poem. I opined once that Sinéad ought to have thrown poor W.B. a credit and an Irish Friend said “it’d be superfluous, every Irish schoolkid has to learn that poem”.

This is one of the great vocal performances ever recorded by anybody, sung in a dozen different voices it seems; hard to believe that so young a throat could cover this range, or so young a mind write this song.

Sinéad’s had some seriously rough patches in her life and it’s hard for her to be happy. She doesn’t owe the world anything, but the world owes her a lot, just for this one song.

This is part of the Song of the Day series (background).

Links

iTunes, Amazon, Spotify. Now, before the video links, a word of caution: These performances are almost unbearably intense, and I think will be uncomfortable for some to watch. That said, most explosive, really scary, most polished (with a bit of sing-along).

Ian: So much for us not having ride-sharing in B.C.   But in many ways, this suggests the pitfalls of any ‘sharing’ company: no regulation which mandates any form of equity.

mkalus shared this story from Price Tags.

From the NY Times:

The average vehicle speed in Midtown today is just 4.7 miles an hour. That’s 28 percent slower than five years ago. Given that most people can walk up to 4 miles an hour, the human body is sometimes Manhattan’s fastest mode of transportation. …

The good news is that modern societies have developed a solution to the tragedy: Charge money to use the commons. Doing so not only discourages overuse, it also raises funds that can solve the larger need — to grow another field where cows can graze, say, or to build a well-functioning subway system. And, yes, I realize that both grazing cows and well-functioning subways sound far-fetched to today’s New Yorkers.

The charge for using clogged roads is known as “congestion pricing,” and it works well where it has been tried, like London, Singapore and Stockholm. In New York, the daily charge to drive below 60th Street might be around $8, with additional charges for vehicles that linger all day. …

The reason more cities haven’t adopted congestion pricing, (past London Mayor Ken) Livingstone says, is “political cowardice.” People cling to the idea that driving should be free, even though it imposes big costs on others.

In New York, (Mayor Bill) de Blasio opposes congestion pricing. He instead favors a millionaires’ tax to pay for subway improvements. Higher taxes on the rich are a fine idea, but won’t unclog roads. For that, de Blasio has offered a series of small, complex measures, like banning deliveries during rush hour. Good luck enforcing that one.

(New York Governor Andrew) Cuomo is more positive about congestion pricing, but has not filled in the details. He may ultimately support a charge only on taxis and companies like Lyft, Uber and Via. That’s a strangely anti-environment compromise, because it encourages people to own their own cars. The New York of the future should have fewer space-clogging cars, not more.

The most serious argument against congestion pricing is that it hurts lower-income workers. That argument also falls apart on inspection, though.

Only 3 percent of poor and near-poor outer-borough workers drive into Manhattan for their jobs, the Community Service Society of New York found. A whopping 61 percent take the subway or bus.

I understand why politicians are afraid to support congestion pricing. We all like the idea of a free lunch — or a free road. But political leadership is supposed to be just that: leadership. It involves making tough decisions for the common good and winning over citizens.

Price Tags: B.C. is at the moment when it can establish the principle of congestion pricing on service providers like Uber et al. The current study, and the Legislative response that follows, need to do that as part of the deal* to allow their entrance into the market, and on the roads publicly paid for, or government will be fighting a rear-guard action when all the opposing forces will be focused on killing congestion charging or mobility pricing.

*Another requirement: the public reporting of all data generated by Uber or any other “transportation network company.”  New York City, which has that requirement, has discovered that congestion in midtown Manhattan is significantly worsening, even as taxi use drops, because of TNCs.  (Story here.) 

More importantly, a transportation network depends on accurate data, especially as we move to real-time management.  Those who have data have power.  If it isn’t the public sector, it will be the private sector – who will then have profound but unaccountable impact on the life and design of the city.  

Apple has launched a new iPad trade-in program in Canada, offering up to $380 in credit towards a new iPad for qualifying devices.

Of course the key word in the above sentence is “qualifying devices.”

In terms of estimated value, Apple offers up to $70 for the iPad 2, up to $170 for the iPad Air, up to $240 for the iPad Air 2, and up to $380 for an iPad Pro.

It’s worth noting that unlike past trade-in offers from Apple, this recycle program is powered by Brightstar and not Phobio. Those interested can check out the value of their current iPad through a simple online questionnaire. For example, my first-generation 16GB iPad Mini is worth a grand total of $85, which isn’t actually a bad deal when you consider how old that device is. That said, an iPad 2 in good condition is just worth $70.

Qualifying iPads need to power up and function normally, be in good condition, must be free of liquid damage, the display must work, and finally, all buttons must be operational. All items must also still have a serial number.

Online trade-ins need to be then mailed-in to ensure they qualify for the program. Trade-ins can also be done in-store.

You can learn more about Apple’s trade-up program at this link.

The post Apple offering up to $380 in credit for old iPad trade-ins appeared first on MobileSyrup.

While the rollout of the Play Store to older Chromebooks has been slow — tediously so in some instances — there’s good news on that front.

This week, Google updated its list of current Chromebook devices that support the Play Store — and by extension Android apps. The updated list, first spotted by Android Police, includes 10 new Chromebook devices. Notable new additions include the 2015 Toshiba Chromebook 2 and two models from Acer. As in the past, support for the Play Store on some devices is limited to Chrome OS’s beta channel.

See the full list below:

• Acer Chromebook 11 (C740): Stable channel
• Acer Chromebook 15 (CB5-571/C910): Beta channel
• CTL J5 Convertible Chromebook: Beta channel
• Dell Chromebook 13 (7310): Stable channel
• eduGear CMT Chromebook: Beta channel
• Haier Chromebook 11 C: Beta channel
• PCMerge Chromebook PCM-116T-432B: Beta channel
• Prowise Chromebook Proline: Beta channel
• Toshiba Chromebook 2 (2015): Beta channel
• Viglen Chromebook 360: Beta channel

Some of the above devices require that users perform “a one-time file-system migration in order to support Android.” Details on how to do that can be found on the company’s support website.

Any Chromebooks that manufacturers release in the future will come with the Google Play Store pre-installed.

Source: Chromium Via: Android Police

The post 10 new Chromebooks gain access to Android apps appeared first on MobileSyrup.