Computer Science
  • The Logic of Testing

    by Vanessa McHale | Computer Science

    Testing is widespread in programming, but correctness in programming is mostly assured by construction. Testing prods a "black box"; this is appealing in that libraries are presented to users as black boxes, but, as we shall see, it is limited in what it can accomplish for deep logical reasons.

  • Functional Compilers That Stand Toe-to-toe With C's Object Files: a Manifesto

    by Vanessa McHale | Computer Science

    There are some ways that functional programming languages still lack when compared to C; in particular they fail to export their constructs for use in other languages.

  • Theorems vs. Algorithms

    by Vanessa McHale | Computer Science

    Functional programmers vaunt the Curry-Howard(-Lambek) correspondence, as if it endorses the lambda calculus. In fact, it shows the limitations of computer science.

  • Laziness, A.k.a. Computer Science

    by Vanessa McHale | Computer Science

    An established problem in functional programming is the question of evaluation order (see Hudak, ยง2.2). Haskell offers seq; which allows the programmer to magically introduce dependencies in evaluation order and thence subvert lazy evaluation. Sometimes this is necessary; see the foldl foldl' example.

  • All Programming Languages Should Have Linear Types

    by Vanessa McHale | Computer Science

    Much like all dynamically typed languages are poor statically typed languages, typed functional programming languages (corresponding to intuitionistic logic) are subsumed by linear logic. Girard articulates this unity in the logical context. Let us gloss the functional programming side of things.