From 5f95aa4a4d1b5d3dadca7a8f8104027eeb76efd2 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Thu, 7 Nov 2024 10:18:23 -0500 Subject: [PATCH] vault backup: 2024-11-07 10:18:23 --- What is Lobot?.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) 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.