Neel Krishnaswami (#neelk) explains the difficulties of applying #formal-methods to imperative code. #cs
on 02019-02-01#PDF #paper of adding linear types to Haskell. #cs
on 02019-02-01#Lock-free concurrency and optimistic synchronization without #garbage-collection in #Rust. #cs
on 02019-02-01“I guess now is as good a time as any to explain "Mirth". Mirth is a strongly-typed #concatenative functional programming language. Mirth draws a lot of inspiration from monoidal category theory, as well as the languages Haskell, Idris, Rust, Lisp, #Forth, and its namesake, Joy.” #cs
on 02019-02-01#incremental recomputation based on Matthew Hammer’s Adapton and Rust’s incremental recompilation stuff #cs
on 02019-02-01discussion thread on #CS theory, on unusual models of computation like the Rotary Element, Turing machines with tapes over arbitrary groups, Iota, Jot, etc. #math
on 02016-08-01“Adam Yedidia, a PhD student at MIT (but an MEng student when he did most of this work), has explicitly constructed a one-tape, two-symbol Turing machine with 7,918 states, whose behavior (when run on a blank tape) can never be proven from the usual axioms of set theory, under reasonable consistency hypotheses,” bearing somewhat on the question of #abiogenesis. This post includes a short #tutorial on #computability and Busy Beaver numbers. #cs
on 02016-05-04Jon Purdy’s thoughts on statically-typed #concatenative languages like Cat, talking about a new one called "Kitten". #cs
on 02016-04-21#pdf #paper on Push-forth, a higher-order statically-typed #concatenative language derived from Joy and Cat, intended for genetic programming. It has a very nice notation for program states in terms of a two-stack machine. #programming #cs
on 02016-04-21Cat is a higher-order #concatenative language (like Forth, Joy, or PostScript) that is statically type-checked with a type system based on #Hindley-Milner. This post goes into some details of how this works. #programming #cs
on 02016-04-21by abusing let-polymorphism in #Hindley-Milner type systems, you can force the type-checking to be exponential-time complexity. #cs
on 02016-04-20Different variants of the lambda-calculus are differently powerful: “The simply-typed lambda calculus is strongly normalizing (i.e. every term has a normal form) and is thus not Turing-complete.” “A partial lambda calculus is Turing complete. A total lambda calculus [i.e. guaranteed to terminate] with inductive recursion primitives is a linear bound TM. A total lambda calculus without recursion primitives is a push down automaton. For an FSA you’d have to limit passing variables in some way.” “There are polynomial time calculi that can calculate only polynomial time things... Generally they work by doing linear typing.” #cs
on 02016-04-20“Extending Landauer’s Bound from Bit Erasure to Arbitrary Computation”, by David H. Wolpert, showing a minimal bound on the energy consumption of even reversible computation. #physics #cs #entropy
on 02016-01-06