kai-qu

I can do no better than quote Knuth (1974) on the merits of a concretely algorithmic point of view in mathematics generally:
For three years I taught a sophomore course in abstract algebra for mathematics majors at Caltech, and the most difficult topic was always the study of “Jordan canonical forms” for matrices. The third year I tried a new approach, by looking at the subject algorithmically, and suddenly it became quite clear. The same thing happened with the discussion of finite groups defined by generators and relations, and in another course with the reduction theory of binary quadratic forms. By presenting the subject in terms of algorithms, the purpose and meaning of the mathematical theorems became transparent.
Later, while writing a book on computer arithmetic [Knuth (1969)], I found that virtually every theorem in elementary number theory arises in a natural, motivated way in connection with the problem of making computers do high-speed numerical calculations. Therefore I believe that the tradition

kai-qu

But as I learned by trying to copy Monet’s paintings, that idea is completely mistaken (Colorplate 2). It is not possible to reproduce the effect of a Monet painting by jousting mechanically with the canvas, jabbing a dot of paint here and planting another one there, until the surface is uniformly puckered in Monet’s signature texture. A painter who does that will end up with a picture that looks soft and uninteresting, with a dull pattern of swirling circles like the ones left by some electric rug cleaners. A brush that’s loaded with paint and then pushed onto the canvas makes a circle, more or less, but Monet’s pictures do not have any circles in them. There is only one slightly rounded mark in this detail from one of his garden paintings—the blue patch at the lower right—and it’s rectangular, not circular at all. [The painting below is a different one.]

kai-qu

I don't hate math per se; I hate its current representations. Have you ever tried multiplying Roman numerals? It's incredibly, ridiculously difficult. That's why, before the 14th century, everyone thought that multiplication was an incredibly difficult concept, and only for the mathematical elite. Then Arabic numerals came along, with their nice place values, and we discovered that even seven-year-olds can handle multiplication just fine. There was nothing difficult about the concept of multiplication -- the problem was that numbers, at the time, had a bad user interface.

Bret Victor

http://www.fastcodesign.com/1664508/ex-apple-designer-creates-teaching-ui-that-kills-math-using-data-viz

kai-qu

type var = string

type inputVal =
  | Impossible
  | Any
  | Some of exp
  
type inputAssn = var * inputVal
type output = exp

kai-qu

But 
    time But she 
        on 
    face, on Lady feared 
    and feared time and 
    Lady and read 
                cut 
    stone, cut in 
        life; 
    by life; how impassive 

kai-qu

"So ropes of gold are found in rivers.
 
Sometimes these cast off skins are sad-colored and the color catches the eye, 
red and blue stones in the river beaches brought out by patches of white-blue snow.
 
There is an ongoing topological dynamic of enfolding whereby in time matter 
pours into itself with a soft malleable voluptuousness of confection, 
marshmellowy and dimpled. This is the grey tunic of a dream, which when turned
outward reveals the most lustrous and colorful of silks.
 

kai-qu

In nested Ltac calls to "hone_Dns", "finish_planning", 
"IndexTactics" (bound to
fun f =>
  IndexPackage2
   ltac:(fun FindAttributeUses2 BuildEarlyIndex2 BuildLastIndex2 IndexUse2
           createEarlyTerm2 createLastTerm2 IndexUse_dep2
           createEarlyTerm_dep2 createLastTerm_dep2 BuildEarlyBag2
           BuildLastBag2 =>
           IndexPackage1
            ltac:(fun FindAttributeUses1 BuildEarlyIndex1 BuildLastIndex1

kai-qu

    { trMap =
                fromList
                  [ ( Sub "CANVAS"
                    , fromList
                        [ ( "height" , FExpr (OptEval (IntLit 400)) )
                        , ( "width" , FExpr (OptEval (IntLit 200)) )
                        ]
                    )
                  , ( Sub "Colors"
                    , fromList

kai-qu

penrose-0.1.0.2: configure (exe)
Configuring penrose-0.1.0.2...
penrose-0.1.0.2: build (exe)
Preprocessing executable 'penrose' for penrose-0.1.0.2...
[ 5 of 16] Compiling ShapeDef         ( src/ShapeDef.hs, .stack-work/dist/x86_64-osx/Cabal-1.24.2.0/build/penrose/penrose-tmp/ShapeDef.p_o )

/Users/katherineye/Desktop/Code/penrose/src/ShapeDef.hs:529:58: warning: [-Wtype-defaults]
    • Defaulting the following constraints to type ‘Double’
        (RealFloat a0)
          arising from a use of ‘findDef’ at src/ShapeDef.hs:529:58-74

kai-qu

{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, NoMonomorphismRestriction, ConstraintKinds #-}

-- Minimal AD example with polymorphism.

import Numeric.AD

type Autofloat a = (RealFloat a, Floating a, Real a, Show a, Ord a)

f :: (Autofloat a) => [a] -> a
f [x, y] = x^2 + y^2 + 0.1