16 lines
988 B
Markdown
16 lines
988 B
Markdown
- 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
|