robsimmons

Programming Language Checklist
by Colin McMillen, Jason Reed, and Elly Fong-Jones, 2011-10-10.

For the Dusa programming language, https://dusa.rocks

You appear to be advocating a new:
[ ] functional  [ ] imperative  [ ] object-oriented  [ ] procedural [ ] stack-based
[ ] "multi-paradigm"  [ ] lazy  [x] eager  [ ] statically-typed  [x] dynamically-typed
[x] pure  [ ] impure  [ ] non-hygienic  [ ] visual  [ ] beginner-friendly
[ ] non-programmer-friendly  [x] completely incomprehensible

robsimmons

robsimmons

#### First proof I wrote ####
Given ~A & ~B
[ Suppose A | B
  [ Suppose A
    ~A          # By conjunction elimination left with (2)
    F ]         # By negation elimination with (5) and (4)
  [ Suppose B
    ~B          # By conjunction elimination right with (2)
    F ]         # By negation elimination with (8) and (7)
  F ]           # By disjunction elimination with (3), (4-6), (7-9)

robsimmons

import { hammock } from "@calculemus/oli-hammock";
//import * as widgets from "@calculemus/oli-widgets";
import { Set }  from "immutable";

type box = { value: string; correct: boolean };
const emp = { value: "", correct: false };

function renderBox(box: box, id: string) {
    $(`#${id}`).val(box.value);
    if (box.value === "" || box.correct) {

robsimmons

// A non-empty rope is either a leaf (string) or a node with two children
// that are both non-empty ropes

interface Tagged<T> {
  tag: T;
}
type RopeNode =
  | Tagged<"node"> & {
      left: RopeNode;
      right: RopeNode;

robsimmons

CREATE TABLE `feedback` (
   `job` int NOT NULL,
   `task` char(20) NOT NULL,
   `payload` longtext NOT NULL,
   `timestamp` timestamp NOT NULL DEFAULT CURRENT_TIMESTAMP,
   UNIQUE KEY `job` (`job`, `task`),
   CONSTRAINT `feedback_job` FOREIGN KEY (`job`) REFERENCES `job` (`job`) ON DELETE CASCADE
);

robsimmons

Original puzzle: https://twitter.com/tausbn/status/251686364788170752

First observation: 

If G ->* {0} implies G =>* {0}, it must be the case that if 
G -> G' and G' =>* {0} then G =>* {0}.

Proof: Given G -> G' and G' =>* {0}, we have G' ->* {0}
immediately (->* contains =>*) and G ->* {0} by direct
composition (G -> G' ->* {0}). Then we have G =>* {0} by the

robsimmons

\documentclass[12pt,openany]{article}

\begin{document}

\setcounter{page}{51}

Basically just read \cite{And01}.

\begin{thebibliography}{WCPW02}

robsimmons

structure A = 
struct
   val say = fn () => print "A\n" 
end

structure B = 
struct
   val say = fn () => print "B\n"
end

robsimmons

datatype foo = A | B | C | D
(*[ datasort ab = A | B ]*)
(*[ datasort bc = B | C ]*)
(*[ datasort abc = A | B | C ]*)

(* This works *)
(*[ val x: ab & bc ]*)
val x = B

(* This, however, does not...