danesabo/Obsidian
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

vault backup: 2024-11-07 10:18:23

Browse Source
This commit is contained in:
Dane Sabo 2024-11-07 10:18:23 -05:00
parent ee29ca438c
commit 5f95aa4a4d
1 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
What is Lobot?.md
View File

@ -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.