Projects
Formal validation of computational python
Python and Lean4 integrations, as structured docstrings, acts as a custom python3 wrapper / linter for CI/CD of computational mathematics and proofs that must hold for certain files, i.e. numpy could eventually use this to show their math library holds and eventually language equiveland, although this was a limitation as its not mathematically possible to show equivelance but it is possible to fluff test random values for each input as this is a formal verification tool between a functional and imperitive language which are inherintly incompadible.
Embedded and hardware validation
STM32U2 embedded step counter, supporting a custom hardware based kernel, rewritten from a software based kernel, custom ICP between host/bare metal, RTOS optimisation methods, written with c and python, there is also support for a custom TCP via a wire so the host machine (windows/macos) could communicate the sensor readings from the step counter during testing to validate the device was operating correctly.
Latex based intractive learning management system
File first method, written as standard latex, and in some cases transferrable from lecture notes, which is then used with code generation to create symbolic mathematics quizzes, programming quizzes with tests, lecture PDFs, and a custom latex editor similar to overleaf in the sense that it is the code file on the left and rendered output on the right.