A few months back I was pessimistic about AI, and now I am the opposite. The perspective change happened when I realized giving it an entire problem and expecting it to solve that is unrealistic. The real value add is if you can use AI at the right steps of your workflow or larger system.
I did a PhD in program synthesis (programming languages techniques) and one the tricks there was to efficiently prune the space of programs. With LLMs it is more much more likely to start with an almost correct guess, the burden now shifts to lighter verification methods.
I still do not believe in the AGI hype. But I am genuinely excited. Computing has always been humans writing precise algorithms and getting correct answers. The current generation of LLMs are the opposite you can be imprecise, but the answers can be wrong. We have to figure out what interesting systems we can build with it.
Do you mean Ruby lacks syntactic support for adding type annotations inline in your programs?
I am one of the authors of RDL (https://github.com/tupl-tufts/rdl) a research project that looked at type systems for Ruby before it became mainstream. We went for strings that looked nice, but were parsed into a type signature. Sorbet, on the other hand, uses Ruby values in a DSL to define types. We were of the impression that many of our core ideas were absorbed by other projects and Sorbet and RBS has pretty much mainstream. What is missing to get usable gradual types in Ruby?
Can you list the concrete problems a FastAPI approach will have, and what tools like Nvidia Triton do differently to get around it? I have no idea about running such models at scale.
The idea that symbolic AI lost is uninformed. Symbolic AI essentially boils down to different kinds of modeling and constraint solving systems, which are very much in use today: linear programming, SMT solvers, datalog, etc.
Here is here symbolic AI lost: any thing where you do not have a formal criteria of correctness (or goal) cannot be handled well by symbolic AI. For example perception problems like vision, audio, robot locomotion, or natural language. It is very hard to encode such problems in terms of formal language, which in turn means symbolic AI is bad at these kind of problems. In contrast, deep learning has won because it is good at exactly these set of things. Throw a symbolic problem at a deep neural network and it fails in unexpected ways (yes, I have read neural networks that solve SAT problems, and no, a percentage accuracy is not good enough in domains where correctness is paramount).
The saying goes, anything that becomes common enough is not considered AI anymore. Symbolic AI went through that phase and we use symbolic AI systems today without realizing we are using old school AI. Deep learning is the current hype because it solves a class of problems that we couldn't solve before (not all problems). Once deep learning is common, we will stop considering it AI and move on the to the next set of problems that require novel insights.
It is already here to be honest. I know BrowserStack and other mobile testing platforms (at Facebook and Amazon) do host real devices, both Android and iPhones, in server farms like this. Meta wrote a blog post about it: https://engineering.fb.com/2016/07/13/android/the-mobile-dev...
At one of my previous workplaces, we discussed running the Z3 theorem prover on an iPhone cluster, because they run so much faster on A series processor than a desktop Intel machine.
This is exactly how Compilers are taught at the University of Maryland. The class CMSC430 (https://www.cs.umd.edu/class/fall2021/cmsc430/) actually starts off with a Scheme (limited subset of Racket) and gradually grows the language to include more features. The first class compiles just numbers to x86 code, followed by arithmetic operations for numbers, building up to higher level features like function calls, pattern matching, and so on. See the notes at: https://www.cs.umd.edu/class/fall2021/cmsc430/Notes.html
There has been attempts as you describe before. I can specifically point to work done in Ruby by my PhD advisor using the exact profiling approach, and then static typing from that: http://www.cs.tufts.edu/~jfoster/papers/cs-tr-4935.pdf
> you're already executing the code for free anyway
Based on my experience of working on similar domain of type systems for Ruby (though not the exact approach you describe), this turns out to be the ultimate bottleneck. If you are instrumenting everything, the code execution is very slow. A practical approach here is to abstract values in the interpreter (like represent all whole numbers are Int). However, this would eliminate the specific cases where you can track "Dict[String->int] WHERE 'foo' in Dict and Dict['bar'] == 42". You could get some mileage out of singleton types, but there are still limitations on running arbitrary queries: how do you record a profile and run queries on open file or network handles later? How do you reconcile side effects between two program execution profiles? It is a tradeoff between how much information can you record in a profile vs cost of recording.
There is definitely some scope here that can be undertaken with longer term studies that I have not seen yet. Does recording type information (or other facts from profiling) over the longer term enough to cover all paths through the program? If so, as this discussion is about maintaining code long term, does it help developers refactor and maintain code as a code base undergoes bitrot and then gets minor updates? There is a gap between industry who faces this problem but usually doesn't invest in such studies and academia who usually invests in such studies but doesn't have the same changing requirements as an industrial codebase.
I have experienced something similar as well. I was visiting NYC, and the place we booked did not look anything like the online listing showed. Regardless, the hosts were nice and helpful, so I left them a 5 star rating on all parameters except cleanliness. This was the first time rated something on Airbnb that is not 5 stars, and I have travelled quite a bit before.
Few weeks after that I receive racist messages from the host on my personal cellphone. I am shocked Airbnb would share my personal details just like that. I reported it to Airbnb, but they were pretty clueless as this was happening outside their messaging system. I finally had to share screenshots of the text messages, and they said they will take down the hosts account. They did for sometime, but after a couple of months that host's account is still live and his place is still accepting reservations. My review has been taken down though.
This seems to be an instance of concolic execution which has seen some success in the fuzzing and testing research community. The key ideas originate from these papers:
The technique works well when parts of the program space (including paths through the program) can be easily represented in SMT solvers (like booleans, bit vectors, and arithmetic), and the remainder program space can be explored using random testing. I am excited to see this work being brought to Crosshair in Python via Hypothesis!
Natural language is ambiguous, so I do not think any programming by example methods will work well here. I think if you are working with a limited vocabulary in the set of sentences you want to parse, it may be fine to roll out a handmade solution. For general english, there is work in intent identification in NLP that can give you structured intents from raw english text, which can then be lifted to make programs as a secondary step.
We apply the Occam's razor here. For a given problem, a smaller program that solves the problem is a preferred solution. It is not a very good metric, and it is fine to disagree with it. But getting a "best" solution, requires one to define what "best" is, and there is no such agreed definition for code.
> The majority of "useful" tests either are stand-ins for what the language should have given you anyways (proper type checking), or they find and fix known bugs, e.g. the intersection of three features.
Find and fix known bugs is one aspect of it. You are not accounting the entire philosophy of test driven development, where one specifies functionality as tests upfront, and later writes code to pass those tests. Anyhow, we have found large projects like Discourse [1], Gitlab [2], Diaspora [3] have tests that specify code behavior well enough so that RbSyn can synthesize them. Very few tests are type-checking, bug fixing and intersection of 3 features.
> Write a test, which proves for all real numbers, that y = 2 * x.
Tests by definition do not prove any for all property. They just check on correctness on concrete values. Formal properties are great for proving properties on values, i.e., for your example one could easily write a logical formula and hand it off to a SMT solver for synthesis and there is enough prior work on that.
> Tests can't fully specify code - this effort is doomed to be incomplete.
RbSyn addresses a different problem: it is difficult to formally specify the behavior of an application in a high-level language that handles HTTP requests, accesses the database. Incompleteness of tests are an advantage here--it allows the specification to be tractable (these are tests programmers would have written anyway), while constraining the search space enough for the synthesizer to give a solution. In practice, it turns out these tests are good enough to synthesize methods from a lot of production grade Ruby on Rails web apps (https://arxiv.org/abs/2102.13183).
It is a hard task, for sure! But without any tests to convey your intent as a programmer, RbSyn also has no way of knowing what you intended a method's behavior to be.
The running thread here is if you would have written a method and some tests to check that you indeed wrote the method correctly, RbSyn will automate the task of writing the method for you. In other words, it is just like test driven development, where the writing the code part is automated.
By manual audit, I meant you can verify if you need more tests to capture your intended behavior or just take a shorter route and update the synthesized code directly without any new tests for the newly added behavior. One could argue the latter is bad programming practice.
That is a fair concern. The tool only guarantees correctness up to the level checked by the tests you provide. So if all corner cases are not covered, RbSyn will generate some program that passes the tests, but might not pass unspecified corner cases. I suspect the missing cases will be clear with a manual audit of the synthesized code, and you can add update the synthesized code manually or add requisite tests.
Indeed, there is rich prior work on example based program synthesis. Often these use inductive logic programming or aided by SMT solvers if these examples can be lifted to solver level values (think integers or booleans, or data types made from those).
However, not all program values can be easily lifted to solvers. So the goal with RbSyn is to allow the programmer to write the same tests they would have written anyway to check their program correctness, without any extra fiddling. As tests subsume examples, we expect more program behavior can be specified than just using simple examples.
> I do wonder if the benefit will really be significant enough to make it worth it.
I have often pondered on what makes a program synthesis tool useful. I expect writing code as art as much as it is science, and people like to express code in the way they model system behavior in their head. In that regard, I do not think program synthesis tools will enable you to automate away large parts of code, but I do think it will automate mundane parts of a program; like writing utility methods, or filling in a partial program when enough information can be gathered from surrounding context (such as the arguments you write for a substring function).
> But doesn't this just mean that instead of writing your code and logic in Ruby you're writing it in RDL?
RDL allows the specification of types and effect labels only. You still write the tests in standard Ruby and synthesized code should satisfy the logic as checked by the tests.
> Also, it would be great to see some examples in the README or in an examples folder. It's kind of hard for me to tell exactly what I need to write and what to call to generate the Ruby.
Sorry for the sparse documentation, I plan to improve that. I have added an example to the readme. Other examples can be found in `test/benchmark` folder.
Hey, nice work with Sorbet! I am one of the grad students who worked on RDL, one of the early research projects related to Ruby type systems. What are the next set of challenges that a tool like Sorbet needs to solve? I see you mentioned meta-programming in the blog post, is that something that is handled well by Sorbet? Sorry if this is already handled, I haven't been up to date with the latest features of Sorbet.
Ruby is and will be the same language even after static types. A Ruby programmer will need to opt-in to writing type annotations in an external file and run a separate type checker (that is not a part of MRI binary). The benefit is if libraries ship with type definitions, type inference can detect type errors early in the IDE. If no type definitions are available, you do not get ahead of runtime type errors.
What you are looking for are refinement type systems. LiquidHaskell [0] is the most well known refinement type system out there, to specify and verify these kind of assertions.
I did a PhD in program synthesis (programming languages techniques) and one the tricks there was to efficiently prune the space of programs. With LLMs it is more much more likely to start with an almost correct guess, the burden now shifts to lighter verification methods.
I still do not believe in the AGI hype. But I am genuinely excited. Computing has always been humans writing precise algorithms and getting correct answers. The current generation of LLMs are the opposite you can be imprecise, but the answers can be wrong. We have to figure out what interesting systems we can build with it.