CS Quotes

[csquotes-blog]

I have emphasised that a meta system allowing non-canonical objects to be treated as indirect proof notations for a represented object system [aka tactics] must have total functions, and be expressive enough to specify which judgement a `thm` object proves.

Robert Pollack, On extensibility of proof checkers

[csquotes-blog]

It was Reynolds who observed that types are useful for syntactically enforcing levels of abstraction, and what that really meant to Reynolds is that one can locally establish invariants for -- and change private representation of -- abstract data types (ADTs), without affecting the observable behavior of code that relies on those types. From my perspective, the crucial point here is that types *enable* programmers to write more reliable code because the burden of establishing invariants on an ADT is kept *local* to the module that defines it. The restrictions of the type system then guarantee that the rest of the program, by virtue of being forced to respect the abstraction of the ADT, is also forced to respect the ADT's locally-established invariants. Thus, the very restrictiveness of types is what enables program *correctness* to scale.

Derek Dreyer, The Types Forum

[csquotes-blog]

Now we want to be able to understand this logic. And to understand the logic, the only solution we have is to make a calculus out of [it].

Gérard Berry, Constructive semantics, electricity propagation in circuits, 2-adic numbers, and formal verification

[csquotes-blog]

Memoization is the conversion of functions to data structures.

Conal Elliott, A trie for length-typed vectors

[csquotes-blog]

There is a strong analogy between using a named operation in a program regardless of "how it works" and using a theorem regardless of how it has been proved.

E. W. Dijsktra, Structured Programming