## Inspiration

Fully homomorphic computing is a hip new crypto trick that lets you compute on encrypted data. It's pretty wild, so I wanted to try something wild with it.

FHE has been getting getting super fast - boolean operations now only take tens of milliseconds, down from minutes or hours just a few years ago. Most applications of FHE still focus on computing known functions on static data, but it's fast enough now to host a real language all on its own. The function I'm homomophically evaluating is *eval*, and the data I'm operating on is code. "Brainfreeze" is what happens if you think about this too hard too long.

## What it does

Brainfreeze is a fully-homomorphic runtime for the language [https://en.wikipedia.org/wiki/Brainfuck](Brainfuck).

## How I built it

I wrote Python bindings for the TFHE C library for fast FHE. TFHE only exposes boolean operations on single bits at a time, so I wrote a framework for assembling and evaluating virtual homomorphic circuits in Python.

Then I wrote an ALU for simple 8-bit arithmetic, and a tiny CPU for dispatching on Brainfuck's 8 possible operations.

## Does it work?

No! I didn't have time to finish the entire instruction set - only moving the data pointer (< and >) and incrementing and decrementing the data (+ and -) work right now :-/. It turns out that computers are complicated and I don't remember as much of 6.004 as I thought I did.

## Could it work?

Definitely at small scales! But there are some severe limiting factors. FHE guarantees - mathematically - to leak **absolutely no** information about the data it's operation on, and that results in a sort of catastrophically exponential branching nightmare because the computer has to execute *every possible instruction on every possible memory address **during every single clock cycle***, because it's not sure which is the "real" data or the "real" instruction and which is just noise.
## Inspiration

We want to share the beauty of the [Curry-Howard isomorphism](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) and automated proof checking with beginning programmers. The concepts of Types and Formal Proofs are central to many aspects of computer science. ProofLang is to Agda the way Python is to C. We believe that the beauty of mathematical proofs and formal verification can be appreciated by more than CS theorists, when taught the right way. The best way to build this intuition is using visualizations, which is what this project aims to do. By presenting types as containers of variants, it allows a teacher to demonstrate the concept of type inhabitation, and why that is central to automated theorem proving.

## What it does

ProofLang is a simplified, type-based, programming language. It also comes with an online interpreter and a real time visualization tool, which displays all the types in a way that solidifies the correct type of intuition about types (with regards to theorem proving and the [calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions)), alongside the instantiations of the types, showing a ledger of evidence.

## How we built it

We wrote ProofLang the programming language itself from the ground up based on the [calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions), but simplified it enough for beginner audiences. The interpreter is written in Rust and complied down to WebAssembly which is imported as a Javascript library into our React frontend.

## Challenges we ran into

We ran into challenges integrating WebAssembly with our React frontend. `web-pack` compiles our Rust code down into Javascript for Node.js rather than the Web JS that React uses. Since the interpreter is written in Rust, there was some fighting with the borrow-checker involved as well.

## Accomplishments that we're proud of

We are proud of building our own interpreter! We also created a whole programming language which is pretty awesome. We even wrote a tiny parser combinator framework similar to [nom](https://docs.rs/nom/latest/nom/), since we could not figure out a few edge cases.

## What's next for ProofLang

Support for function types, as well as type constructors that are not unit-like! Going forward, we would also like to add a visual programming aspect to it, where users can click and drag on a visual interface much like [Snap](https://snap.berkeley.edu/) to write code, which would make it even more accessible to beginner programmers and mathematicians.
## Inspiration

We enjoyed playing the computer party game [*Keep Talking and Nobody Explodes*](http://www.keeptalkinggame.com/) with our friends and decided that a real-life implementation would be more accessible and interesting. It's software brought to life.

## What it does

Each randomly generated "bomb" has several modules that must be defused in order to win the game. Here's the catch: only one person can see and interact with the bomb. The other players have the bomb defusal manual to defuse the bomb and must act as "experts," communicating quickly with the bomb defuser. And you only have room for three errors.

Puzzle-solving, communication, and interpretation skills will be put to the test as players race the five-minute clock while communicating effectively. Here are the modules we built:

* **Information Display** *Sometimes, information is useful.* In this display module, we display the time remaining and the serial number of the bomb. How can you use this information?
* **Simple Wires** *Wires are the basis of all hardware hacks. But sometimes, you have to pull them out.* A schematic is generated, instructing players to set up a variety of colored wires into six pins. There's only one wire to pull out, but which one? Only the "experts" will know, following a series of conditional statements.
* **The Button** *One word. One LED. One button.*
Decode this strange combination and figure out if the button saying "PRESS" should be pressed, or if you should hold it down and light up another LED.
* **Password** *The one time you wouldn't want a correct horse battery.* Scroll through letters with buttons on an LCD display, in hopes of stumbling upon an actual word, then submit it.
* **Simon Says** *The classic childhood toy and perfect Arduino hack, but much, much crueler.* Follow along the flashing LEDs and repeat the pattern - but you must map it to the correct pattern first.

## How we built it

We used six Arduino Unos, with one for each module and one for a central processor to link all of the modules together. Each module is independent, except for two digital outputs indicating the number of strikes to the central processor. On breadboards, we used LEDs, LCD displays, and switches to provide a simple user interface.

## Challenges we ran into

Reading the switches on the Simon Says module, interfacing all of the Arduinos together

## Accomplishments that we're proud of

Building a polished product in a short period of time that made use of our limited resources

## What we learned

How to use Arduinos, the C programming language, connecting digital and analog components

## What's next for Keep Talking Arduino

More modules, packaging and casing for modules, more options for players