diff --git a/What is Lobot?.md b/What is Lobot?.md index 969050307..c8ffcfeb7 100644 --- a/What is Lobot?.md +++ b/What is Lobot?.md @@ -1,3 +1,14 @@ - Lobot is a sublanguage of Lando. - What the fuck is Lando? - - + - Something that converts natural language to something lower in the stack +- So what is Lobot? + - Well lobot apparently is 'well documented' and does a lot of type things. + - Sets up the environment and makes functions available to the user + - It is a specification language. This is the meat of setting up properties and allowable actions + - Section 5.3.3 is one big stinky piece of shit. +- last line: 'the full Lobot specification of th eRTS system is found in **??**' +- There is whole bunch of these everywhere in the document I got from the NRC. This thing stinks. +- Lobot seems to basically just create the space of all possible results and ensure that variables have the types you require. +- It looks like these get passed down to an actual theorem prover or whatever FRET is. +- Lobot has 'consistency checks' at the end of the file that are baby theorems. +- The github is FULL of todos.