No doubt that developments with dependent types and the formally-provable code movement (I feel like I can call it that) is worthy of attention. Wrt Manin's (and by extension Knuth's) comment, I almost see this movement as bearing fruit functorially in the mathematics community[L]. Playfully, I see it as being analogous to what happened when American filmmakers saw what Italian filmmakers were doing with American westerns.
The value, in the long run, of provable code I sincerely have hope for. Not only do I see value there for the engineer of critical applications, but also for the systems-level thinkers that will need to have a bridge between ever higher-level abstractions and the ever complexifying bytecode beneath. There, in that Daniel Murfet paper cited some months ago on the *Derivative of a Turing Machine*[D], I even sense a future where tight formal logic guides the design of neural networks. Manin cites Euler and Gauss, and from the bit of Euler's original work that I have read, he was clearly a *sit by the fire and calculate endless pages of computations when one cannot sleep* kind of guy. Equally, no one would accuse him of avoiding the challenge to prove. I would not be surprised if a great deal of his best theorems were not inspired by a desire to simplify calculations and from observing the data produced by his computations. I believe that the perpetual desire to refactor and port over to new frameworks shares sympathy with this sit-by-the-fire approach, and the dawn of the computer has provided this tendency, new domains to inhabit. [L] Clearly, computation has its roots in the logical community, it's proto-languages, those of Turing and Church, predate the first mechanical implementations, and ever since that community has never *really* strayed far. [D] http://friam.471366.n2.nabble.com/Derivatives-of-Turing-Machines-td7599131.html -- Sent from: http://friam.471366.n2.nabble.com/ - .... . -..-. . -. -.. -..-. .. ... -..-. .... . .-. . FRIAM Applied Complexity Group listserv Zoom Fridays 9:30a-12p Mtn GMT-6 bit.ly/virtualfriam un/subscribe http://redfish.com/mailman/listinfo/friam_redfish.com FRIAM-COMIC http://friam-comic.blogspot.com/ archives: http://friam.471366.n2.nabble.com/
