Cur: Designing a less devious proof assistant

William J. Bowman�University of British Columbia

The Deviousness of Proof Assistants

The Deviousness of Proof Assistants

“The tools we use have a profound (and devious) influence on our thinking habits, and therefore our thinking abilities.”

​

• Edsger Dijkstra

Dijkstra, E. W. How do we tell the truths that might hurt. Selected Writings on Computing: A personal Perspective. 1982. pg 129--131. doi:10.1007/978-1-4612-5695-3

The Deviousness of Proof Assistants

The Deviousness of Proof Assistants

e ::= λx:A.e | e e | x | ()

The Deviousness of Proof Assistants

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

The Deviousness of Proof Assistants

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

The Deviousness of Proof Assistants

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

What is that?

The Deviousness of Proof Assistants

Inductive e : Set :=

| lam : x -> A -> e -> e

| app : e -> e -> e

| var : x -> e

| unit : e.

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

The Deviousness of Proof Assistants

Inductive e : Set :=

| lam : x -> A -> e -> e

| app : e -> e -> e

| var : x -> e

| unit : e.

​

Error: The reference A was not found in the current environment.

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

The Deviousness of Proof Assistants

Inductive e : Set :=

| lam : x -> A -> e -> e

| app : e -> e -> e

| var : x -> e

| unit : e.

​

Inductive A : Set :=

| Arr : A -> A -> A

| Unit : A.

​

Error: The reference A was not found in the current environment.

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

The Deviousness of Proof Assistants

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

Inductive x : Set.

(* Out of scope for this talk *)

​

Inductive A : Set :=

| Arr : A -> A -> A

| Unit : A.

​

Inductive e : Set :=

| lam : x -> A -> e -> e

| app : e -> e -> e

| var : x -> e

| unit : e.

The Deviousness of Proof Assistants

...

​

Inductive e : Set :=

| lam : x -> A -> e -> e

| app : e -> e -> e

| var : x -> e

| unit : e.

​

Fail Check lam.

​

e ::= λx:A.e | e e | x | ()

A B ::= Unit | A -> B

x ::= infinite collection of names

“λ” by itself is an error

Error: The command has not failed!

Ought I think this way?

Ought I think this way?

But how exactly can an "ought" be derived from an "is"?

My belief: proof assistants ought be less devious

The moral philosophy of Cur

The moral philosophy of Cur

​

The user should be free to express how they think, not forced to think like their tool.

The moral philosophy of Cur

​

The user should be free to express how they think, not forced to think like their tool.

Therefore, the tool should enable the user to develop their own ways to think and express themselves.

So how do we free the user?

Desiderata

1. The surface language is extensible and redefinable

“... a good notation sets [the mind] free to concentrate on more advanced problems, and in effect increases the mental power.”

• A. N. Whitehead

Whitehead, A.N. Introduction to Mathematics. 1911. pg 59. http://libgen.is/book/index.php?md5=2DBE153E8FE5081F31A761766244E779

Desiderata

• The surface language is extensible and redefinable
• The foundation is extensible and redefinable

“I’m skeptical of the unspoken assumption that there’s an underlying concept of a ‘foundation’ … What matters is these jobs we want our theories to do and how well they do them.”

• Penelope Maddy

Maddy, P. What Do We Want a Foundation to Do?�Reflections on the Foundations of Mathematics. 2019. 293-311. doi:10.1007/978-3-030-15655-8_13

Desiderata

• The surface language is extensible and redefinable
• The foundation is extensible and redefinable
• Extension development and composition is a first-class linguistic feature

“When programmers must resort to extra-linguistic mechanisms to solve a problem, �the chosen language has failed them.”

• PLT Design Inc., The Racket Manifesto

Felleisen, M.; Findler, R. B.; Flatt, M.; Krishnamurthi, S.; Barzilay, E.; McCarthy, J. A. & Tobin-Hochstadt, S.� The Racket Manifesto. SNAPL. 2015.�doi:10.4230/LIPIcs.SNAPL.2015.113

Surface Language Extension

Typical proof assistant

Core

Elaboration

Surface

Typical proof assistant

Core

Elaboration

Surface

Hooks for user-extension

Cur

Curnel

Cur

Elaboration

Hooks for user-extension

Cur

Meta-language

Curnel

Cur

Elaboration

Racket

Hooks for user-extension�(macros)

Cur

Object-language

Meta-language

Curnel

Cur

Elaboration

Racket

Shallow Embed.

Racket

Hooks for user-extension�(macros)

Demo 1--3

1. Intro. to Cur
2. Adding template meta-programming

Core Language Extension

Cur

Object-language

Meta-language

Curnel

Cur

Elaboration

Racket

Shallow Embed.

Racket

Hooks for user-extension�(macros)

Lies, and damned lies!�(no statistics)

Cur’s actual archieture

Cur

extends

racket

The Macro Expander Long May it Rein

Define default language features

Redefine & remove language features

Language-oriented Design

racket

extends

racket/base

The Macro Expander Long May it Rein

Interpret “lambda” this way.

Interpret “lambda” this new way.

Language-oriented Design

racket

extends

racket/base

The Macro Expander Long May it Rein

Register “lambda” transformer

Replace “lambda” transformer

Language-oriented ~ Prototype object-oriented

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented ~ Prototype object-oriented

• Declare prototype

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented ~ Prototype object-oriented

• Declare prototype
• Preserve `super` methods

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented ~ Prototype object-oriented

• Declare prototype
• Preserve `super` methods
• Declare methods/overrides

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented ~ Prototype object-oriented

• Declare prototype
• Preserve `super` methods
• Declare methods/overrides
• define-syntax = (re)define methods

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented ~ Prototype object-oriented

• Declare prototype
• Preserve `super` methods
• Declare methods/overrides
• define-syntax = (re)define methods
• Left-paren “(” = Invoke method
• Default method is #%app

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented ~ Prototype object-oriented

• Declare prototype
• Preserve `super` methods
• Declare methods/overrides
• define-syntax = Define methods
• Left-paren “(” = Invoke method
• Default method is #%app�����
• (yes, that means “require”, “provide”, and “define-syntax” are also overridable)

#lang racket/base

​

(require

(only-in racket/base

[lambda super.lambda]

[#%app super.#%app]))

​

(provide

(rename-out

[new-lambda lambda]

#%app)

​

(define-syntax new-lambda ...)

​

(define-syntax #%app ...)

​

((new-lambda (x : Nat) x) 1)

​

Language-oriented Design

Transformers can:

• Construct/deconstruct syntax
• Associate metadata with syntax
• Control expansion order
• Generate new transformers
• Access binding information
• Use compile-time state
• Run arbitrary computation

racket

extends

The Macro Expander Long May it Rein

Replace “lambda” transformer

racket/base

Cur and Language-oriented Design

Transformers can:

• Construct/deconstruct syntax
• Associate metadata with syntax
• Types
• Control expansion order
• Generate new transformers
• Access binding information
• Use compile-time state
• Parameterize language �by typing relations
• Run arbitrary computation
• Type checking logic

Cur

extends

The Macro Expander Long May it Rein

Replace “lambda” transformer

racket

Cur and Language-oriented Design

Since Cur is “just macros”, �everything happens during expansion

• Macro expansion (of course)
• Normalization by macro expansion
• Evaluation
• Type checking

Cur

extends

The Macro Expander Long May it Rein

Replace “lambda” transformer

racket

Chang, S.; Knauth, A. & Greenman, B.

Type Systems As Macros. POPL 2017.

doi:10.1145/3093333.3009886

Chang, S.; Ballantyne, M.; Turner, M. & Bowman, W. J.

Dependent type systems as macros.PACMPL., 2020, 4, 3:1-3:29�doi:10.1145/3371071

Pédrot, P.-M.; Tabareau, N.; Fehrmann, H. J. & Tanter, É.

A Reasonably Exceptional Type Theory PACMPL 2019, 3:ICFP, 108:1-108:29�doi:10.1145/3341712

Demo 4�Extending Cur with RETT

Unsolved Problems

Not really Unsolved Problems

• Separate, Trusted Kernel
• Possible, but we haven’t done it, and the design makes it harder.
• Limiting/Tracking User Extensions
• Possible, but we haven’t done much on it. Requires overriding the module system.
• Performance
• Quadratic expansion. Expansion algorithm was designed for outside in, not inside out.
• No sharing/hash consing in syntax objects. Really vital for dependent type performance.
• Diamond Problem
• Like in OO with multiple inheritance, multiple extensions can be annoying.

Unsolved Problems

• What are the semantics of macros even?
• Big problem: open-recursive binding manipulation.
• Many grad theses lay abandoned on this hill.
• Can we generate proof-of-soundness obligations from a user’s extension?
• Expand to a language boundary, not fully
• Currently expands completely to core Racket. We’d like to expand to Curnel and then stop and do work.
• Michael Ballantyne @ Northeastern is working on a new macro expander design.
• Resugaring
• Lots of work, but still an open problem.

Designing a less devious proof assistant

​

The user should be free to express how they think, not forced to think like their tool.

Therefore, the tool should enable the user to develop their own ways to think and express themselves.

“The tools we use have a profound (and devious) influence on our thinking habits, and therefore our thinking abilities.”

​

• Edsger Dijkstra