- 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. - Lots of 'what the fuck?'s