lambda-mountain
lambda-mountain copied to clipboard
andrew-johnson-4
Compact Typed Assembler (5K SLOC)
These two modes shouldn't require separate codepaths on the backend. Currently some things are just hard-coded and hard to change dynamically.
In Coq total functions must return a value matching their type signature. Exceptions and failures are not permitted. This could be added as a modifier to functions that can't fail.
Coq `Prop` are sound but *reallly* nasty to use. For now the verifier can do projects to check nominal types, then project those nominal types onto their properties in Coq....
Proofs with partial knowledge should still be model checked against actual architecture specifications: * https://github.com/maximedenes/coq-amd64
start by asserting hello world example
* [x] check that memory state satisfies a constraint (also expressed as a memory state) * parse assertions from gnu assembly * yield assertions to Coq proof * [x] break...
This would make implementation of Lisp or Scheme standards almost trivial. Then these languages would have implicit access to system interfaces and C/C++/Rust libraries.
It might be nice to distribute binary objects with separate proof annotations not in the same file. `objdump` can be used to disassemble and then annotations can be inserted.
Declare an empty list from unascripted constructor. Use list as list of concrete type like u64. The type inference should work but currently needs more than one pass.
