lambda-mountain
lambda-mountain copied to clipboard
andrew-johnson-4
Compact Typed Assembler (5K SLOC)
``` declared f : U64 -> U64 actual f : U64 -> I64 ``` error may happen in *call-sites* to this function, whereas they maybe should highlight the function body...
A lot of the basic algorithms could be much condensed by functors instead of functions
Start with simpler concepts like blob rendering and build up to coq verified x86. Don't rush.
Accept patterns like below in lhs context ``` [ 1 , 2 .. rst .. 7 , 8 ] => ... ```
Automatic Coercion Classes can be thought of as an unspecialization of that argument. No-coercion functions are still preferred, but if an automatic coercion exists, then that can fit if nothing...
``` (==( (head-string a) (head-string b) )) ``` segfaults
Documentation should not require a specific framework. It should be fairly generic at a basic semantic level.
There should be no reserved words. keywords are acceptable based on syntactic position, but all identifiers should be valid in identifier position.
serialization / deserialization primitives should * be polymorphic over fallibility (can it fail) * be polymorphic over culpability (what should happen if it fails) * be polymorphic over totality (is...
normally chaining just concatenates two S-Expressions. However there needs to be special chain rules for context or stack offset. context and stack offset should use the most recent value rather...