chas

Taking pure to mean referentially transparent, I'm not sure I understand your point here. If you are mutating a statically allocated struct or array passed by reference, doesn't that have a very similar effect to global variables? It makes the dependence explicit rather than implicit which is useful, but it is still effectively global state.

Coq isn't based on HoTT, however, the people working on HoTT use a modified version of Coq in conjunction with a library that contains the essential elements. https://github.com/HoTT/HoTT

I am not a mathematician and I can't speak to the likelihood of a mathematical revolution, but as a programmer with interest in theoretical computer science and I found the HoTT book to be extremely useful. Prior to last year there were very few available and approachable resources for learning HoTT. Papers on the subject were hard to find and harder to understand for someone not in the field. Because of this, any textbook is a huge step forward for me even if it doesn't have mass appeal because it allows people who aren't directly researching HoTT to become familiar with the ideas and results and find further references to previous work. These people in turn can educate others who might be computationally or mathematically inclined and interested in the benefits of HoTT such as better interactive theorem proving, but don't have specific interest in type theory, category theory, or homotopy theory and therefore find existing resources difficult to understand.

Every time Douglas Engelbart is in the news, I reread Bret Victor's reminder of his goals. http://worrydream.com/Engelbart/

GPUs have been used effectively in implementing graph algorithms. Graph algorithms are tremendously useful and show up all over computing.

http://arxiv.org/abs/1002.4482

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.220...

You might also be interested in CMU's introductory curriculum in the same vein which is somewhat less extreme and has a particular focus on parallelism as the standard case of computing. http://existentialtype.wordpress.com/2012/08/17/intro-curric...

That is a function that takes a starting parameter and returns a pair with the length of the sequence as the first element and the starting value as the second element. This is mapped over a list of integers from 1 to max_a0 to find the length of the sequence starting with each integer.

Maximum finds the largest component of a list and compares on the first element of a pair first, so the pair with the longest sequence length as its first element and the starting value that produced that sequence length as it's second element will be returned by `maximum $ map (\a0 -> (collatzLen a0, a0)) [1..max_a0]`.

This function could also be expressed as `collatzLen >>= (,)`, if you were into that sort of thing.

The processor chip itself is designed as a DFA (as is very common in digital logic design though EEs prefer the term finite state machine or FSM). These slides do a good job of explaining this perspective on digital design. [1]

It becomes much more powerful when given the ability to read and write from arbitrary storage, they same way theoretical DFAs become turing machines when given the same power.

I am glossing over the complications that on-chip caches and memory hierarchy introduce, but I feel the core idea of a processor chip as a DFA is still worthwhile.

[1]http://www-inst.eecs.berkeley.edu/~cs150/fa05/CLD_Supplement...

A PC can still read and write from arbitrary memory locations which means it can know a lot about it's past states, so the memory limit makes it a deterministic linear-bounded automata.

http://en.wikipedia.org/wiki/Linear_bounded_automaton

Another way of saying this is that the two stacks as a list zipper[1], which makes the correspondence between a DFA with arbitrarily writable memory and a DFA with two stacks readily apparent.

[1]http://en.wikipedia.org/wiki/Zipper_(data_structure)#Example...

Not really. Haskell is basically used as a compiler from a DSL to C. Compilers running on general purpose systems are much less sensitive to timing and memory use than embedded systems and kernel drivers, so it isn't that big of a deal. The generated C code is the only thing that executes on the target device so you get the same performance that you would expect from C code.

Absolutely! I am very interested by their approach in this area because integration with existing infrastructure is essential for practical work in this area, but reasoning about existing infrastructure is a lot harder than it needs to be.

This is a relatively old presentation of theirs, but it has a decent overview of what they have used Haskell for. http://www.cse.chalmers.se/edu/year/2010/course/TDA555/Mater...

This is really neat, but I am very wary of building kernel modules with garbage collected languages especially ones like Haskell, which can has very difficult to reason about runtime characteristics due to laziness.

One approach that I find much more promising is using Haskell (or other robust and semantically easy to reason about and easy to verify languages) to generate C code which then can be used with normal toolchains for low-level development. Galois is doing a lot of work in this area that looks very promising. One of their projects is an autopilot system called SMACCMPilot[0] that uses a Haskell eDSL called Ivory[1] to generate safe C code. I am particularly excited about its integration with FreeRTOS tasks using the Tower Language[2] (another Haskell eDSL).

This makes it possible to generate code that can be reasoned about with Haskell but has the runtime characteristics of C. This is particularly interesting because embedded systems code is notoriously non-composable and difficult to reason about due to the enormous shared state of the hardware itself and the highly concurrent nature of interrupt-driven design. Embedded C makes a good target for this sort of design and analysis though, because it has very constrained memory usage (developers typically eschew dynamic allocation), very subtle potential issues (debugging race conditions with LEDs sucks), and very serious consequences for errors[3].

[0]http://smaccmpilot.org/index.html

[1]http://smaccmpilot.org/languages/ivory-introduction.html

[2]http://smaccmpilot.org/languages/tower-overview.html

[3]http://en.wikipedia.org/wiki/Therac-25

Most likely things like version control, static analysis, dynamic analysis (e.g. Valgrind), automated testing, and code review. The Joel Test[0] is a good starting place.

[0]http://www.joelonsoftware.com/articles/fog0000000043.html

Many software developers don't work with FOSS technology at work. I work in embedded systems and much of the library code I work with has been provided by manufacturers of the devices I'm using. I do find bugs in it and report fixes to the library developer, but they often have strange licensing and don't use github (or even public version control) so this work doesn't end up visibly attributed to me in public.

This doesn't mean that the people working in non-web industries "are not playing in the same league" with respect to skill, it just means that they don't have a huge public representation of the work they do.

This doesn't help in quite the way you would like, but the recursion limit is adjustable through sys.setrecursionlimit [1].

[1]http://docs.python.org/2/library/sys.html#sys.setrecursionli...

It is important to note here that that many automakers allegedly demand extremely high quality code from themselves. The MISRA C standard [1] is widely used as a guide for high quality embedded code in many industries and was developed by the Motor Industry Software Reliability Association.

[1] http://en.wikipedia.org/wiki/MISRA_C

The basic idea is that it is possible to transform a signal without loss of information from being some value vs time (so called time-domain signals) to being a bunch of different frequencies with different intensities (so called frequency domain) where the frequencies are just sine and cosine waves. A pure sine wave in the time domain gets transformed into just one value with the same amplitude as that wave in the time domain.

To see why this is useful, imagine a song you wanted to listen to that was recorded with a low-pitch hum in the background because the microphone running next to a power cable and picked up the 60 Hz signal. Removing this unwanted tone by looking at the value of the song in time is really hard because the 60 Hz signal is mixed up with the rest of the song. However, when transformed into the frequency domain, the 60 Hz hum is very easy to spot and remove. When you transform the signal back into the time-domain (so you can listen to it), the 60 Hz will still be gone.

This process can be done automatically with computers using a technique called the Fast Fourier Transform. This is the basis of many techniques in the field of Digital Signal Processing (DSP) which is the theory behind most of the communication breakthroughs of the last 40 years. I should note that many naive approaches to this problem (like the approach in my example) don't work particularly well, so as in any problem domain, there are important but subtle performance trade-offs to consider.

[1] http://www.dspdimension.com/admin/dft-a-pied/

You might know this, but I want to state it at least for the benefit of people reading this without much signal processing experience. Just zeroing like that really isn't the best idea. Square waves (that are 1 for signals that you want and 0 for signals you don't want) inverse Fourier transform to sinc functions[1], so if you are filtering just by chopping things out, it will greatly distort the time-domain system because the inverse Fourier transform of the filter and the signal get combined (convolved) in the time domain.

[1] http://en.wikipedia.org/wiki/Sinc_function

If you want low-overhead pseudo-concurrency for C, protothreads [1] are probably what you are looking for.

[1] http://dunkels.com/adam/pt/

The programming language trolling in the article is building a language with strong static types controlled entirely by naming convention, specifically hungarian notation, rather than normal type declaration. http://en.wikipedia.org/wiki/Hungarian_notation

That is the first line of Anna Karenina: "Happy families are all alike; every unhappy family is unhappy in its own way."

Total functional programming (and the associated analysis of codata has already been touched on), so I'll just address your interest in static guarantees for space usage. The Virgil programming language[1] has been designed with exactly this in mind. It is aimed at embedded systems where memory is extremely constrained and running out of memory could kill people. Heap allocation is not possible in the language and all data structures are initialized during compilation (like C++ templates, but more sophisticated). The compiler can use the initialization information for advanced optimization and analysis as well as serving as a bound on the memory usage. [2] The language also has some interesting static typing ideas, but they are not as distinct from other languages.

Further discussion on LtU: http://lambda-the-ultimate.org/node/2131

[1] https://code.google.com/p/virgil/ [2] http://compilers.cs.ucla.edu/virgil/overview.html

I have heard good things about the Apache Portable Runtime [1], GLib [2], and Sglib [3] if you want something a bit more stripped down.

[1] http://apr.apache.org/ [2] https://developer.gnome.org/glib/2.34/ [3] http://sglib.sourceforge.net/

Bret has previously given a talk[1] that addresses this point. He discusses the importance of using symbolic, visual, and interactive methods to understand and design systems. [2] He specifically shows an example of digital filter design that uses all three. [3]

Programming is very focused on symbolic reasoning right now, so it makes sense for him to focus on visual and interactive representations and interactive models often are intertwined with visual representation. His focus on a balanced approach to programming seems like a constant harping on visualization because of this. I think he is trying to get the feedback loop between creator and creation as tight as possible and using all available means to represent that system.

The prototypes I have seen of his that are direct programming tend not to look like LabView, instead they are augmented IDEs that have visual representations of processing that are linked to the symbolic representations that were used to create them. [4] This way you can manipulate the output and see how the system changes, see how the linkages in the system relate, and change the symbols to get different output. it is a tool for making systems represented by symbols but interacting with the system can come through a visual or symbolic representation.

[1] http://worrydream.com/MediaForThinkingTheUnthinkable/note.ht...

[2] http://vimeo.com/67076984#t=12m51s

[3] http://vimeo.com/67076984#t=16m55s

[4] http://vimeo.com/67076984#t=25m0s

Never and ten years[1] feel pretty similar in month two.

[1] http://norvig.com/21-days.html

He's playing fast and loose with the formalisms to try to convey the intuition to people without a strong algebraic background. Ruby isn't very well behaved from a categorical perspective (heck, even Haskell doesn't get all of the way there if you want to be really formal) so it's not perfect, but I think the reasoning is morally correct and insightful.

Homotopy type theory[1] is essentially working to show that math is (or can be viewed as) an interesting application of computer science.

[1] http://homotopytypetheory.org/2013/06/20/the-hott-book/

The logo is nice, but the aliased angled lines really kill it for me. I think a vector (or better anti-aliased) logo would really make a positive difference in the feel of the site.

Reading through this book[1] was a really mind-expanding experience for me. It is an overview of the kernel and doesn't dive into any one part in depth, but it was extremely valuable for me in learning how to structure a large c project as the same techniques and ideas are useful for many large projects.

[1] http://www.amazon.com/Kernel-Development-Developers-Library-...