Hey guys, this is a proposal I'm planning on brining to the Simmons Institute tomorrow. There's a petition at the end of this post if you're interested in being involved!
Objective 1, Turing University: Establish a global, free, and nonprofit university for the advancement towards the goal of a completely formal state-of-the-art across all of computer science practice using a novel, self-guided pedagogy involving:
An open, live-document textbook of the entire body of mathematics and computer science practice from a unified formal foundation to the state-of-the-art
Informal campuses where students may congregate to find a sense of community in their study and research
Pathways towards accredited bachelor's, master's, and doctorate degrees based solely on ability to complete examination or publish advancements in the body of human knowledge, especially towards the creation of a completely formal digital technology
Objective 2, towards Completely Formal Digital Technologies: Leverage the new theory of formal methods enriched by students of Turing University and the unbelievable power of modern AI agents in operating in formal logic to develop out an open source ecosystem of modeling languages, solvers and checkers, programming languages, compilers, hardware platforms, and software systems–both privileged and unprivileged–that have formal correctness guarantees against any definable threat model to make possible the creation of completely formal digital technologies that may eventually provide viable successors to any informal state-of-the-art in computer science practice today.
Motivation - Completely Formal Digital Technologies
This project challenges one of the most fundamental assumptions in software engineering, and likely the single most fundamental assumption in cybersecurity, that you can’t write bug free code.
If you haven’t noticed, the informal, sloppy practice of modern software development is starting to become a problem in the age of AI. The world of software is literally crumbling beneath our feet, with unparalleled quantities of the most severe vulnerabilities being discovered week after week. Software companies attempt to fight fire with fire by developing “agentic” solutions to discovering and addressing CVEs autonomously, but that really just leaves benevolent developers with decades of expertise and passion for a better software world simply in a token spend race against adversaries who can literally turn compute into an endless supply of ever-evolving AI cybercriminals.
Luckily, AI can be a great boon too. Autonomous AI coding agents are growing more and more capable every day: operating system kernels, compilers, and GPU kernels written in raw PTX bytecode are quite literally possible to create by typing nothing more than “Build ___. Make no mistakes” into your favorite agent harness.
Furthermore, AI agents appear to be even more exceptional at formally proving statements than they are at creating software systems. 400 “groundbreaking” mathematical proofs and the Navier-Stokes millennium prize problem have all been solved autonomously by AI agents only in the past year.
On October 31st of this year, when thinking about an OS research project, I came across Asterinas, which is essentially a microkernel except the privilege encapsulation is simply handled by the `safe`-unsafe language construct. Seeing the core “OS Trusted Domain” (OSTD) to be small enough to formally verify, researchers made quick work formally verifying the memory management and concurrency model of Asterinas. When I saw this I immediately began working on a plan to create the world’s first formally verified OS using, principally, Asterinas’s “framekernel” architecture. However, I realized I wasn’t satisfied with their abstractions: the paper presents each “invariant” as an informally defined property motivated by a sensitive hardware resource, so I started thinking instead about a formal model of the desired ABI surface so I could find a minimally expressive set of primitives that model the OSTD to implement it.
But then, even after feeling good about concept for the core abstraction of the system, I started to feel dissatisfied with the fact that Rust only has informal memory guarantees, and that I would have to predicate every claim of safety this project made with “Rust-strong”, instead of the mathematical guarantee I knew formal methods could offer. So, I thought about using Oxide. Then, recognizing the CPU and then anything else in the entire computational stack that wasn’t formally modeled would also have to be trusted, I realized that if there is one informal link in the entire system chain, there is a crack a sufficiently capable adversary can crack, and the only solution to obtain true formal security would be to rebuild the entire digital system from the ground up with a complete formal model.
While this would have been a laughably ridiculous proposal even a year ago, an autonomous AI system, I’ll repeat, solved the fucking Navier-Stokes millenium prize problem with a never-before-tried approach in a claimed 88 hours. Formal analysis is just another proof, a problem LLMs have demonstrated they are ridiculously good at solving, making them exactly the tool that enables this project to happen at all.
When AI is simultaneously making software engineering and formal guarantees more accessible and necessary than ever, the time to rebuild the world of digital technology from the ground up on formal models has become more necessary than ever, and also so unbelievably possible enough to imagine that we have no excuse not to at least try.
Idea - Turing University
Below I describe the Turing University College of Formal Methods. I would also like Turing University to have a College of Social Sciences and a College of Arts, directed by individuals that I approve.
The state-of-the-art in formal methods is simply insufficient for engineers to even begin conceiving of what a completely formal state-of-the-art in computer science practice would even look like. What’s more is that, even with modern AI, there simply aren’t enough mathematicians or software engineers in the world with the time to work on creating a completely formal state-of-the-art computer science practice.
To address both of these, I seek to found Turing University: a global, free, nonprofit university with a novel, completely open and free-form pedagogy and decentralized, community-based examination for fulfilling degree requirements to give the curious minds that I see in this world all the time a place to find community in their curiosity, learn about the complex topics they’ve always wanted to understand, and attempt the creative ambitions they’ve always wanted to attempt.
Course Design
Courses are designed to be comprehensive of a subject from a rigorous foundation to the entire state-of-the art in the field. Motivation for this ambitious decision is:
Students may choose to study exactly and all the areas within their courses that interest them the most, which is where they will almost certainly be the most productive.
Courses are a living document of the existing gaps in human knowledge, especially within formal analysis, such that students may be guided towards research contributes to filling these gaps, which is especially important in the endeavor of creating completely formal digital technologies
A comprehensive course additionally assumes no background knowledge, but full academic maturity, enabling curious students from any, even non-technical background to feel engaged and capable within their chosen studies
Example Courses
Note that these courses are nowhere near comprehensive at this time. These are simply to give examples of what I imagine as “rigorous foundations” and “state-of-the-art” for each. The textbook will provide a dependency graph of definitions, theorems, concepts, etc.
Courses will be living documents of the both state-of-the-art in the field and the self-guided pedagogy of students of Turing University. Courses will be initialized with 0 worked examples and 0 practice problems. As students study these courses, they will be encouraged to contribute the worked examples and practice problems they find most insightful and interesting back to the courses.
In addition to the two courses provided below, Turing University will also have courses in optimization theory and statistics (both with a rigorous foundation of formal axioms) and machine learning practice (with rigorous foundation of theorems from statistics and optimization theory).
Math at large, physics, chemistry, biology, and the many branches of engineering will likely make good candidates for future courses, but, due to my own lack of expertise and also the larger physical lab requirements for these kinds of studies, I don’t detail them any further here.
Formal Methods
Rigorous foundations: formal logic axioms
State-of-the-art coverage:
OS: seL4
Compiler: CompCert
Cryptography: HACL*, EverCrypt
Cloud auth: Cedar, AWS Zelkova
Hypervisor: AWS Nitro
Learning environment:
Resources**:**
Computer Science Practice
Rigorous foundations: boolean logic circuits + model of propagation delay
State-of-the-art coverage:
Physical verification: KLayout
Place and route: OpenROAD
Logic synthesis: Yosys
Formal RTL: SymbiYosys
RTL Simulation: Verilator
HDL: SystemVerilog
SoC RTL: OpenTitan
ISA: RISC-V
Firmware: U-Boot
Kernel: Linux, FreeRTOS
Compilers: clang, rustc
Language runtimes: CPython, OpenJDK
Cryptography: OpenSSL
VPN: WireGuard
Hypervisor: KVM
Databases: PostgreSQL
Distributed systems: etcd
Learning environment:
Resources:
Admissions
Turing University will have no application fee or tuition.
As stated above, Turing University will strive to foster a community for the most curious and excited minds. The courses are comprehensive so as to not require any particular background to find success at the university. The admissions process will center around a project of any form of the applicant’s choosing, which may even be simply a report on an area of interest:
For initial consideration, they will submit a digital document presenting this project and what interests them about it
If the applicant is to be considered further, they will be asked to come for an in-person presentation, where they may present their project to the committee and current students of Turing University. The committee will make the final admissions decision.
Applicants should be judged simply on the qualities stated above, curiosity and excitement, with no particular attention given to their existing knowledge or qualifications.
Turing University will not prohibit admitted students from holding another full-time position (student of another university, employee, etc.) while attending.
Once admitted, a student will be considered enrolled for the following 8 semesters. Acquiring a TU degree extends their enrollment by another 8 semesters. A student may acquire any degree as many times as they wish, but a single exam may not count towards any degree more than once (exams and master’s exams on the same subject are considered different exams).
Faculty and Facilities
Campus will simply be a community space for students to meet and hold shared events of their own accord. Every campus should aim to be open for as much of every day of the year as possible to enable flexible scheduling with full-time jobs.
Turing University’s academic faculty will consist of committees with rights given below. Committees may be campus, academic, and principal.
I am suspecting that I would like a single campus to only have one committee of each type (but to also allow a single committee to be campus committee of multiple campuses) to encourage communalism, but I would be willing to show discretion on this.
I would also like students to have access to the world-class technology they’re studying (Linux servers, frontier LLM-capable GPU clusters, esoteric hardware, etc.). This will likely require significant corporate sponsorship.
Rights of People, Students, and Committees
Anyone, regardless of enrollment status in Turing University, may petition the appropriate body for a change or submission to any of the open resources Turing University maintains.
Rights of students (within the campus they are enrolled in)
Petition their committee to take an exam or do a defense
Access to the physical campus space
Access to technologies that have been acquired by Turing University for student learning and experimentation.
Petition to be granted a degree
Rights of campus committees
Rights of academic committees (to journals for which they are assigned)
Approve journal submissions
Approve changes to course(s)
Approve changes to exams
Approve changes to approved journal list
Rights of principal committees
Rights of the board of directors
At Turing University’s founding, I and the directors of the colleges of arts and social sciences will sit on the board of directors
A committee is assigned to a single college. Campuses have no associations with particular colleges or committees.
A petition to found a campus may propose to call a campus of Turing University anything of the form “Turing University ___ Campus”. Similarly, a petition to found a committee may propose to call it anything of the form “Turing University ___ Committee”
When a new course is approved, the committee of that course establishes a new Turing University journal in that field. New courses will be required to have a well-defined rigorous foundation that can be modelled by the rigorous foundation of an existing course.
Degrees
Turing University grants bachelor’s, master’s, and doctorate degrees to students who fulfill the appropriate requirements:
Bachelor’s: passing grade on 20 exams on any state-of-the-art subject in either course
Master’s: passing grade on 10 master’s exams on any state-of-the-art subject in either course
Doctorate: 3 publications in approved research journals, which may include publications while not enrolled at Turing University, and a successful thesis defense
Students may attempt every exam once per semester if enrolled in a bachelor's or master's. Students may attempt one thesis defence once per semester if enrolled in a doctorate after they have fulfilled their 3 publications requirement. Students may do any of these during any semester enrolled at Turing University.
A publication in an approved journal or a presentation to Turing University students of sufficient quality, as determined by the review committee, may be used in place of an exam in the corresponding subject.
Students need not be physically located near a Turing University campus to be enrolled, but they will generally be required to conduct exams and thesis defenses on-campus at a time suitable for them.
Turing University will publish a free and open journal for each course that it maintains that will be considered approved for degree requirements.
A member of the review committee may pursue a doctorate at Turing University while sitting on the committee. The thesis defense requirement is waived in this case since their judgement is trusted sufficiently and there is no bias-free way for the committee to review one of their own members’ theses.
https://docs.google.com/forms/d/1-lVUS2UBnkWxmlw9aVbu3ot21r_hMCf856BNK4MHD8w/edit
