CodeLogician tutorial first draft #217
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
sam-tombury
commented
Apr 15, 2025
Comment on lines
+52
to
+56
| When you're using *CodeLogician*, you're incrementally creating a model of your source code. The are two phases of using *ImandraX* are as follows: | ||
| - Model admitted to *ImandraX* - there are no missing definitions and type-checking passes | ||
| - Model admitted *ImandraX* and executable - there are no opaque functions (either they're fully implemented or substituted with approximations) | ||
|
|
||
| We'll go into approximations in more detail later, but for now you can think of them as *mocking* functionality you don't have access to (e.g. third party services or libraries) or computation that difficult to reason about (e.g. *exp* function). |
There was a problem hiding this comment.
I wonder whether it's preferable to leave the caveat around opaque functions to later in the docs (with its own dedicated section). If we can focus the first section on purely algorithmic problems then users probably won't encounter them immediately, and then we can introduce them gently later on and explain the axes of refinement:
- Assumptions (
axioms), which provide more context to refine the reasoning. - Approximations, which provide more context for model execution (e.g. test case simulation).
| - *Recursion* is used to model (besides recursive functions) loops. So, both `while` and `for` loops will be rewritten as recursive function calls. The key to reasoning about recursion is _induction_ and by rewriting (for example) a `for` loop as call to a recursive function, ImandraX can easily identify the inductive structure. | ||
| - *State machines* - these are typically *infinite* state machines because the *state* type may contain complex datatypes (structures, lists) in addition to the regular arithmetic types. *State machines* are a useful mechanism for modeling code with side-effects (where the variable outside the scope becomes part of the state) and, more generally, complex systems like stock exchanges. For example, you would the stream of incoming order messages as a list that the top-level `step` function iterates through. | ||
|
|
||
| ### What should we model (let's talk about abstraction)? |
There was a problem hiding this comment.
I really like this section. I think it gets to the heart of one of the big questions that people will ask when they see this sort of thing - "where do I use it?".
We should get ahead of people just trying to randomly formalize any Python file they have open (e.g. a FastAPI definition, or some data science utilities) and getting underwhelming results (as the code isn't really algorithmic).
These 3 layers are a helpful tool for explaining that. I see them as basically:
- High-level = Design. Model the design of a system (using a DSL) and use Imandra to verify that the design is sound (and identify any fundamental design flaws).
- Mid-level = Implementation. Code the implementation in your usual language, and use CodeLogician to translate that to a formal model. Imandra then is used to reason about the implementation (e.g. identifying edge cases, finding counterexamples), but we don't make any guarantees about the actual execution of the program.
- Low-level = Execution. At this level, we attribute precise meaning to everything and so can make stronger assertions about the runtime semantics.
Can we make this section more prominent/earlier, so that it grounds the broader context of symbolic AI?
|
|
||
| ### Adding information to models through refinement | ||
|
|
||
| *Refinement* refers to the process of adding more details to the model if it starts with opaqueness present. We think of a model as being in one of four stages: |
There was a problem hiding this comment.
I see this refinement as having two axes:
- Assumptions (
axioms) refine the opaque function for the purpose of reasoning. - Approximations refine the opaque function for the purpose of execution (though naturally there's some overlap when it comes to 'expected results' as an output of region decomp sample points).
| - 2 - the multistep process of *autoformalization* and *refinement* during which the agent uses *ImandraX*, various tools, its database of formalisms (recommended translation samples) and user input to create *model* | ||
| - 3 - the ultimate result will contain recommended changes, verification report and test cases | ||
|
|
||
| The interface to the agent is very flexible - you can ask it to perform the full process of *model* creation, verification and test case generation, or ask it to perform individual steps. This last part is especially useful when you're using it via MCP server through a coding assistant like *Cursor*. |
There was a problem hiding this comment.
Awesome, helpful thing to point out!
hon-gyu
reviewed
Apr 16, 2025
Comment on lines
+180
to
+182
| If you're using *CodeLogician* through a tool like Cursor, then it's quite easy to convert these to English prose (or other formats and languages) or testing framework and language of your choice. | ||
|
|
||
| In a sense, generation of these regions is also generative AI, but the results are derived solely from the logic of the model - no statistics involved! If you're using *CodeLogician* through a tool like Cursor, then it's quite easy to convert these to English prose (or other formats). |
There was a problem hiding this comment.
it's quite easy to convert these to English prose appears twice. is there a mistake here?
|
I'll work on the following
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.