The Piton Project

Piton is a simple assembly-level programming language. A sample Piton program is:

Subroutine big-add(a b n)
       push-constant f     ; push false on the stack
       push-local a        ; push the value of variable a
loop   fetch               ; pop an address, fetch and push contents
       push-local b        ; push the value of b
       fetch               ; pop an address, fetch and push contents
       add-nat-with-carry  ; add the 2 topmost elements
Piton provides execute-only programs, recursive subroutine call and return, stack-based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven type-safe abstract data types including integers, data addresses, program addresses and subroutine names. The semantics of Piton is given by an Nqthm function.

Piton has been implemented on the FM9001, a 32-bit general purpose microprocessor with 16 general purpose 32-bit wide registers, four 1-bit condition code registers and up to 2^32 words of memory. Using Nqthm, Warren Hunt and Bishop Brock proved that FM9001 was correctly implemented by an NDL netlist. That netlist was then fabricated by LSI Logic, Inc.

The implementation of Piton on the FM9001 is via an assembler/linker that maps a system of Piton programs and data declarations into a binary image for the FM9001.

The assembler/linker is written as an Nqthm function. Using Nqthm, I proved (with help from Matt Kaufmann), that Piton is correctly implemented on the FM9001. In particular, I proved
The Piton Correctness Theorem: If then the data produced by the n-step run above can be alternatively produced by

Piton provides a convenient abstract machine upon which one can build compilers for higher level languages. Such compilers have been built and verified (e.g., by Bill Young and Art Flatau). In addition, applications programs have been coded directly in Piton and verified (e.g., by Matt Wilding).

Piton is a part of the CLI Stack, a sequence of languages and/or computing machines, each implemented atop the previous one,

CLI Stack

and involves work by Bill Bevier, Bishop Brock, Warren Hunt, Matt Kaufmann, and Bill Young, in addition to me.

For details of the Piton Project, see

[Best Ideas] [Publications] [Research] [Home]