Add internal project ideas page

ideas-internal.md

@@ -0,0 +1,35 @@
+---
+layout: page
+title: Project Ideas
+permalink: /ideas-internal/
+---
+
+## Education
+
+**CS pedagogy**
+- Nand2Tetris in OCaml/LEAN: Piyush (IITPKD), Patanjali (IITM), Manu (IITGN)
+- Dynamic textbook
+- Intro to CS for non-CS audience: Aalok Thakkar (Ashoka)
+- OCaml notebooks (like Jupyter) that run in the browser
+
+**Lean for elementary mathematics** — Formalise pen-and-paper arithmetic operations (addition, subtraction, multiplication, long division) and basic discrete math proofs in Lean. Goals: (1) teaching material for 1-day beginner workshops on formal verification; (2) potential basis for teaching discrete math at IITM. Collaborators: Pranav Ramesh, [Neeldhara Mishra](https://www.neeldhara.com/) (IIT Gandhinagar).
+
+---
+
+## Systems, Security & Formal Methods
+
+**Cryptographic primitives in OxCaml** — Implement basic cryptographic primitives natively in OxCaml, rather than as C wrappers (cf. [cryptokit](https://github.com/xavierleroy/cryptokit)). Demonstrate the performance and safety benefits of direct OxCaml implementations.
+
+**Lean verification of Bluespec System Verilog hardware** — Use Lean to verify simple hardware designs written in Bluespec System Verilog.
+
+---
+
+## Concurrency & Programming Languages
+
+**Linearizable data structures in presence of data races**
+
+**Memory model 2.0**
+
+**Composable concurrency**
+
+**Linearizability checker for blocking operations**