Skip to content

Commit

Permalink
update
Browse files Browse the repository at this point in the history
  • Loading branch information
mike dupont committed Feb 28, 2024
1 parent 3818757 commit af902fc
Show file tree
Hide file tree
Showing 3 changed files with 36 additions and 7 deletions.
2 changes: 1 addition & 1 deletion 2024/01/07/batteries-included
2 changes: 1 addition & 1 deletion 2024/01/27/coq-of-rust
39 changes: 34 additions & 5 deletions 2024/02/28/notes.org
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,8 @@ to lower artiy ones.
we can think of applications as have large N values in arity
and axioms having very few.

** Meta Introspector

we can imagine that
there is an meta protocol
or meta pattern of introspection
Expand All @@ -100,6 +102,38 @@ which comprises of the following :
13. llms, open models
14. unimath
15. comic books as epic tapestries
16. goedel numbering or quasi quotations as emojis or other languages
17. creation of ebnf grammars
18. training of models and ml ops
19. creation of reproducible builds

All of these things together give you some ideas about points to consider
for introspection and then we
can think of applying this
to an individual problem that
is expressed in this system.
we can look at an error as a point that we can expand
greatly.

* compiler error fixer
create a compiler error fixer
that lives in coq and ocaml and gcc
and python etc as plugin
that generically passes the error context
to the llm for fixing.
us introspection
and the univalent point of
view that all bugs are instances
of human invention,
aka techincal debt.

If we are able to rewrite some text using
computers preserving the meaning
then we can see it as understandable.
even if it is not understandable to
other people immediatly.
we can think of the llm as kind of
a proof assistant.

* license

Expand All @@ -122,8 +156,3 @@ here are some commands i ran:
find -name \*.v >vfiles.txt
for x in `cat vfiles.txt`; do grep file -H -n $x; done
#+end_src





0 comments on commit af902fc

Please sign in to comment.