philzook58
commented
3 years ago Honestly, the project is not completely formed conceptually or highly worked on. I tinker with it every once in a while partially as a learning exercise to myself.
What I want is a straightforward, down to earth translation of the machine and language described in the nand2tetris course. It is unclear how achievable this is or what it may mean really to verify it's construction beyond merely describing an emulator of it in Coq. Presumably I will need theorems connecting behavior at the different layers of abstraction.
Currently I think I would go all Coq no Haskell. That is from a time when I was very uncomfortable in Coq. I do agree i should get github pages working. In particular i should use alectryon https://github.com/cpitclaudel/alectryon . I have some more material that is uncommitted.
Bruno-366
apart from formatting issues that impact its readability (which I'll gladly help with), it leaves some questions to be answered, for example it states that coq and other formal tools will be used. So far its seems like the project mainly consist of Haskell, coq, and verilog, is there any plan for this to change? or is the idea, that like for example make a lisp nand2tetris is going to be implemented in as many formal tools as possible? :)