[FRIAM] coding versus music

[jon zingale]

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/