asQuirreL

I don't think this is a circular buffer. The strategy here is to shift the data inside the buffer to the middle once either the front or back pointer are at the front/end of the buffer respectively, rather than to wrap around.

My intuition is that a circular buffer would be better though, because it would not have to do any large scale moves of memory until it came time to reallocate.

I wrote a full implementation of this version in Haskell as part of my dissertation [0]. I'm linking to a specific commit because in the coming month, I will be modifying it to introduce structural type inference (so that what would typically be considered a data type declaration can also be inferred).

[0]: https://github.com/amnn/typed_geomlab/blob/c79c4bbb3179ef66b...

I would argue that the whole point of having a type class is the laws. It allows the programmer to assume certain properties are true that the type checker cannot verify. Just because the language lets you write an instance that does not conform to a class' laws, does not mean it is the right thing to do, it is precisely because the language cannot check them that those laws exist.

In a dependently typed language, types may rely upon arbitrary terms that are computed at runtime, and yet you are correct that dependently typed programs are checked statically. The way this is achieved is if a property can only be checked at runtime, then the burden of proof for that property is moved from the typechecker to the program.

The program must verify the property at runtime and create a witness to the proof, which it can then pass to functions to say that it has done the necessary work.

So I guess the answer is yes and no. I would say the whole point of dependently-typed languages is that we can statically determine that somebody is maintaining correctness, be it at compile time or at run time.

Some types are not (and cannot) be enforced at compile time [0]. In fact what makes something a type is not something internal to the type, but its participation in a larger type system or type theory, so in that sense, almost any abstract model of computation could give rise to types, as long as it was sound.

[0]: https://en.wikipedia.org/wiki/Dependent_type

Any day in which you can say this, is a good day.

This of course assumes the candidate knows the answer to the question they asked, which is something the interviewer can't verify because they also don't know.

This is an interesting point, and one I've seen from the other side as well: When leaving secondary (high) school, for university, a common piece of advice is: "You may have been one of the smartest people here, but be careful, you probably won't be where you're going, so you have to manage your expectations." But if everyone is being told this, then those who could become some of the "smartest people at university", are being told it too, and some of these people could be unnecessarily lowering their expectations. I've always thought this was a great shame.

I'm a bit dubious about your sweeping generalisation that "most mathematicians haven't don't any logic".

I also agree with GP that logic also does not deal with absolute truth. Proofs in formal logic may be applied to models, but they only provide truths modulo the assumptions made in those models.

As for your remark on equivalence. Your original description is one of syntactic identity, a sort of free equivalence. But any relation that is reflexive, transitive and symmetric can be considered an equivalence (indeed, there are infinitely many equivalence relations over the integers). Also note that this is not the same as how "=" is used in computer programs where for the most part it is asymmetric (a=b is rarely semantically equivalent to b=a).

Nice explanation! I believe the short-circuited open `sum` function will evaluate to `1`, though.

Well, I would say it exposes a flaw in your interface, which would have given the function access to more information than it required. You know it's fine because you are aware of implementation details, but rust is telling you that your interface doesn't reflect that.

Not in figures, but a graph was given in the article that shows the sample distribution.

It is possible that some people teach for the enjoyment and gratification of it. Some of my lecturers are excellent programmers.

Good programming skills are not necessary to teach CS, but that does not imply that teaching CS is a sufficient condition for having bad programming skills. (Propositional Logic 101, taught by someone who may or may not be good at programming).

Couldn't reply to the child post, so I'm putting it here:

Yes it is true that if a company helps but does not entirely solve a problem, they are not obligated to stick it out. But in this case it may be that they are not helping by offering homeless people seasonal jobs. The fallacy here is that homeless people have a choice: if I were in a desperate situation, then I would take any job on offer. I.e. by being given the option the decision has essentially been made for for me, and whilst I may be better off in the immediate future, that doesn't mean it will last (and it could even be worse in the long term), and whilst I could decline the offer, and wait for something more stable, my circumstances are sufficient motivation for me not to do that.

A cynical person might even posit that by explicitly not doing enough to bring people out of homelessness, Amazon succeeds in maintaining a pool of willing and cheap seasonal labour.

On a similar theme, this year there is a conference called Wadlerfest [1] running in Edinburgh in honour of Phil Wadler's 60th birthday.

[1] http://events.inf.ed.ac.uk/wf2016/

> Cool. I’m glad to see Pascal has adopted Rust’s approach of putting the type last, so you can actually see at a glance what the variable names are.

I'm guessing (hoping) this is irony...

It is an imaginary machine, intended to have restrictions that most real hardware wouldn't have (like not being able to access the BAK register directly), but the aim of this is to make the game more of a challenge, and thus more fun.

> Well, computer "science" is primarily an engineering discipline.

I would say that software engineering was the engineering discipline, and computer science a mathematical discipline.

My point was that the proof itself is not subsidiary to empirical evidence, only its application is, and in my eyes, there is merit in the proof, free from its application to the "real world", for example as a lemma to another proof. Consider it a form of separation of concerns: whilst I prove a theorem, I am not concerned with how it mirrors the observable world, but in order to apply it, of course I must ensure that its assumptions can be reliably observed. In this way, our "beliefs" are limited and do not taint the logic of the proof itself.

> How do you know that while these proofs reference the infinite, they are actually applicable to the infinite?

Which brings us to your next point: I do not know, I simply believe it to be true because it is convenient to do so. My point is that this belief or its refutation does not affect the worthiness of the proof, only that of its application.

I actually do not believe in the absolute power of proof, I don't think it is something you can get away with believing once presented with all the facts. I hope I've explained myself better in this comment though: I don't think our views are as antipodal as it first seemed.

I prove mathematical properties purely for the sake of proving them. The fact that they have any bearing on the real world is a mildly interesting diversion. Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.

I feel like the analogy would be "writing mathematical proofs without writing down any of the propositions" (And indeed, the Curry-Howard correspondence lends credence to this). Writing down types for programs is not just useful because the computer can check them, but also because it commits what is in one's mind.

What's more, type-checkers offer a lot more help in checking types than Coq does at proving mathematical propositions (There is a reason, after all, that one is an assistant, whereas the other is a checker), so, relatively speaking, writing a proof without Coq is not as hard as typing a program without a type-checker.

A lot of the observations in this article are very interesting, but personally, I drew different conclusions.

The first one is the main thesis of the post which is that some people have an innate ability to program that others do not possess, and that this is a thing that cannot be learnt. As a result, telling people that it is "easy to code" is a lie.

Firstly, it is actually not clear to me that this ability to pick up programming principles cannot be taught. All we know is that our current methods of teaching yield a double hump distribution for programming ability.

Secondly, if people were actually saying "you will find coding easy" to anyone and everyone then I agree that they are probably concealing the truth. But actually, if you read the tagline on the example given (The Year of Code initiative) it says:

> Start coding this year, it's easier than you think.

"It's easier than you think" (emphasis mine). This is quite a different statement to a flat out "it's easy", and it's one I agree with. To most people, coding appears difficult because they simply don't know the answers to a few key questions (E.g. Where do I write the code? What do I do to run my code? How does the computer understand what I've written?). The (basic) answers to these questions are comprehensible to most people, and furnish them with the ability to write code (maybe not well, but that's a whole other story).

Next observation:

> Folks, which industries/professions give up their own free time to provide free/open training to people wishing to enter the sector? Curious

The fact that only the software development industry seems to do this is painted as a negative thing in the article. Why is that? I ask because this is a fact I think we should be proud of. I personally enjoy what I do so much, that I happily spend time out of my week, teaching it to others for free. I don't do this because I think all the people I teach will go on to become successful software engineers, but rather because I want to widen the net, and expose more people to what we do, because for some of them (maybe even just one of them) this might be their "true calling".

I got into programming originally from watching a cousin of mine editing the themes of his Wordpress blog. He went on to study English Literature and Psychology; To him, coding was just this tool that allowed him to publish his views, but to my 9 year old self, watching him, it really struck a chord and I was hooked. Now, there is not a thing in the world I could imagine myself doing rather than writing code and loving every minute of it (And no amount of "social status" is going to turn me to a life of law, medicine or architecture). What an opportunity I would have lost if I had not seen my cousin working on his blog... Every week-long learn to code course, and every "hour of code" initiative works towards bringing such opportunities to the wider public.

Finally, on the role of Computer Science degrees: I am currently in my final year of a Masters in CS, which I have also enjoyed studying immensely. I would not say that it has contributed directly to my skills as a software engineer, but the things I have learnt have changed the ways in which I approach problems. Very few people write structural induction proofs, loop invariants or abstract specifications to prove the correctness of their programs, but I have found them to be great ways to think about how to write better code. These skills, however, are complementary to those that make a good software engineer, not a substitute. There's no way to prove yourself out of a rat's nest of class hierarchies and control structures.

Oh yeah, I totally agree, the examples for the IO monad match up very well to what can be done with Promises. My point was more that this is the case because the IO monad is the canonical black box monad: All you can do with it stems from its implementation of the monad interface, and so anything that behaves like a Monad will look very similar. This is tantamount to saying that Promises have a potentially useful Monad instance (which I am completely in agreement with you on).

The point about continuations is also a very interesting one, but I think again, stems from the same idea: Almost any monadic interface can be simulated with continuations.

Not sure promises are equivalent to the IO monad in particular. They could form a Monad instance, although that is not the interface they have chosen to expose. It does seem it would be more similar to the `Either` monad, however.

But not into a register right? Given my (flawed) assumption that there would be two reads, whilst the first might load the second into the cache, it wouldn't load into a register without another instruction telling it to. This costs a lot less than the cache fetch but it still has a cost.

Also worth noting that storing them in a long probably means 2 memory reads per access on most modern architectures, whereas storing them in bitfields will allow the compiler to select the containing CPU word, which will be 1 read. I would be interested to see actual performance measurements (maybe a performance vs memory usage chart).

Some notes about using sets to represent types:

Firstly the symbol you are using for "subset of" is in fact the symbol for "strict subset of". This means you are saying that when C : A + B there is some value that implements A and B but that is not accepted in the place of C. This is of course, simply not true.

Secondly, Type theory itself was created in part due to the inadequacies of Set theory, which is why it is tempting to find parallels in the two, but it will only go so far.

Imagine oneself playing a game of Simon Says, where we don't know who Simon is or which bits he's actually saying, he in fact sounds exactly like everyone else giving us instructions: we can choose to believe what we want about the actions we are told to make, but an adversarial Simon can always contradict us. It's not a game I'd enjoy playing nor a lesson I think I benefited from very much...

From a Computational Learning Theory perspective, we are faced with an infinite hypothesis space, with an infinite VC dimension. So yes, there's not much strategy that can be employed here.

But, the fact that there is one correct answer is not really an assumption that the puzzle makes, it is information we have been given:

> We've chosen a rule that some sequences of three numbers obey -- and some do not.

This simply means that the solution is realisable. No matter how many ways (in English) we have to describe that solution it is still the same solution.

It took me until:

> Hashes are always O(1) reads, inserts and writes.

To realise that this was a joke.

You don't know ruby yet.