sankha93

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

This style of building compilers is called the Nanopass style (https://legacy.cs.indiana.edu/~dyb/pubs/nano-jfp.pdf), making it much easier to teach.

Source: I was a TA for the earlier iteration of the class.

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:

[1] https://web.eecs.umich.edu/~weimerw/590/reading/p213-godefro...

[2] https://mir.cs.illinois.edu/marinov/publications/SenETAL05CU...

The Wikipedia page gives a good overview of the area and some successful applications: https://en.wikipedia.org/wiki/Concolic_testing

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.

> Best solution? Most easily maintained?

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.

[1]: https://github.com/discourse/discourse [2]: https://github.com/gitlabhq/gitlabhq [3]: https://github.com/diaspora/diaspora

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

Thanks for the feedback! I just uploaded a video now that demos RbSyn in action: https://www.youtube.com/watch?v=yYAOK5S8lRY

The concepts, capabilities, and limitations of RbSyn are explained in this talk: https://www.pldi21.org/poster_pldi.124.html with full details in the accompanying PLDI paper: https://arxiv.org/abs/2102.13183

I will link these from the readme soon.

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.

[0]: https://ucsd-progsys.github.io/liquidhaskell-blog/

> Learning languages is big investment, and having dozens of languages around is not productive, human languages are consolidating over a few, English is by far the business language of the world

> Why does language design continue to be a subjective topic? its not like computers need cultures !

Learning languages are a big investment, that is indeed true. But the comparison with English is flawed - human languages are very ambiguous by nature and often the meaning is inferred based on the context we use words. This is often apparent when one wants to write something unambiguous in English: for example, a document that is legally binding - because you want to make things as precise as possible. Most legal documents hence define terms and then use them with meticulous detail. Indeed writing these down is such a complex task that we have an entire profession dedicated to them - lawyers. So put in another way what the lawyer is doing is defining abstractions for that document and then using them to write the binding terms and conditions in the document.

How is this related to programming languages? Well, a similar argument would be we should all use assembly for programming since that is what the CPUs use anyway. You are not wrong, but that would mean so much wasted effort by programmers to define basic abstractions for every program they will ever write. Programming languages are nothing but abstractions for the problem you are solving. And problems programmers solve vary wildly - a OS or driver developer worries about vastly different problems than a data scientists and their languages show that. This is why computer do not need "cultures", but programmers do. A kernel level programmer worries about manual memory management, and handles raw pointers on their own. A data scientist just cares about manipulating tables and training models. How the memory is managed is an extra detail that is not relevant to the problem domain and languages like Python provide an abstraction for that (a garbage collector).

This is why it is always good to experiment with languages. Probably 1 in a 100 language will become mainstream, but what these experiments give us are a medium to see what abstractions work successfully to represent programs in different domains. This is how object-oriented programming or garbage collectors are mainstream today. As far as Nim goes, I think it is a language that allows you to ship compiled native binaries without manual memory management with lots of Python like language features. So the intended audience is for people who want to ship binaries but want to use expressive features like iterators, etc like Python provides.

I agree with the mathematical rigor required for abstract interpretation. I am arguing that there is a lot of value in thinking about programs that operate on other programs as interpreters. Essentially interpreter doesn't have to be equivalent to the evaluation of a program.

My pet peeve is with all static analysis articles like this is they demonstrate how to solve a particular problem, but never talk about the universal abstraction that allows one to write any static analysis tool: interpreters. Really, all you need to do is write an interpreter.

A standard interpreters for a language (like Python) evaluates the language to produce some value. If you want to do static analysis, make the values the property you are analyzing. In this blog post's example the value is a boolean denoting whether a file is a test file or not. Thus an interpreter would be recursive on individual AST nodes, doing the decisions shown here in the sample and returning the expected value from the analysis. This forms the core of a rich literature in abstract interpretation, where the program analyzer instead of producing the concrete results of evaluating a program produces a the value of a property that you want to analyze.

Even compilers are interpreters. Instead of writing ad-hoc methods that do some operations, compilers can often be structured as something that evaluates the a program in source language and instead of producing a value, produces another program in a different language.

Interpreters are underrated!

Edit: typos

This article is a classic example of Facebook PR doing a wonderful job of selling the research and linked paper [1] claiming too much in the introduction. Please, please talk to actual researchers before you buy such claims.

If you go through the paper - you have to check the evaluation section to see how they measured their success. They used some programs from GeeksforGeeks to evaluate their approach. Problems on GeeksforGeeks do not represent the vast majority of programming tasks encountered in daily life. This is very much in contrast to the overarching claims presented in the introduction of the paper.

Second issue with the evaluation: they use BLEU scores to judge how good their translations are. BLEU makes sense for natural language translations (even that is widely debated in the NLP community these days). For a program there is no concept of an almost correct program (based on how things look similar), it is either correct or not. Eg. if I am asked to write a program to add two numbers and I write `x - y`, I am not almost correct, I am completely wrong. And in some ways that is what their model does, it optimizes for BLEU scores.

Third, the correctness of the programs are tested based on 10 random inputs. Are 10 random inputs enough to cover the entire input space that can be accepted by a program?

It is indeed a great advance in the application of ML technology, but it is nowhere close to the broader claims. One can even debate, ROI on time spent in gathering and curating data and then checking the correctness of translation from such system vs the ROI on writing rules for a rule based system since all programming languages are easily expressible that way.

[1]: https://arxiv.org/pdf/2006.03511.pdf

University of Maryland teaches Rust for a single lecture as a part of their CMSC330 (Organization of Programming Languages) [1] undergraduate class. The lecture slides are available online [2].

[1] https://www.cs.umd.edu/class/spring2020/cmsc330/

[2] https://www.cs.umd.edu/class/spring2020/cmsc330/lectures/25-...

I am from a computer science background. I understand basic biology and genetics. I have been trying to understand what are reasons why code and that cells are biological computers is a poor assumption. Anecdotal evidence like the SARS-COV2 you mentioned or things I hear from biologist friends mostly along "it is not so simple". Are there good studies that shed light on what are the missing pieces and how can we simulate/model biological processes better?

The article doesn't try to use any feature of the web platform, but tries to piggy back on it to provide their own runtime functions. WebIDL could be a overkill in such a scenario. Usage of WebIDL means there is a bindings generation process using a Python script during compilation of servo.

I could imagine one can define all the functions available in the JS runtime using the same facilities that are used to define the intrinsic objects like Array, Number and so on. Their implementation could use an event loop provided by Tokio.

Comparison with Deno is interesting and could provide interesting insight into how SpiderMoney can be used to build such a runtime. I tried to build one at https://github.com/ngsankha/rustynode couple of years ago, but abandoned due to other commitments. The implementation is far from optimal.