4 ms·

Hi! I was the TA for this course in 2020, and did my Ph. D. under the professor. Ask me anything.

squircle 2y ago
Hi @Darmami, what have you been working on in the meanwhile? Given the current state of programming and compsci research, what interests you these days? (What do you see as most important 5 to 10 years down the road?) As a layperson I don't have time to grok most of this but revisit from time to time.
- Darmani 2y ago
  Hi Squircle! I mostly left academia after graduating, and am not actively following current research, although I still live in Cambridge and attend a fair number of research events. I can say that deep learning has taken over PL research, just like everything else. A good number of PL and synthesis people have shifted heavily into pure deep learning, and a large proportion of those that haven't are working either on applying deep learning and LLMs to solve PL problems, fusing PL and ML techniques (aka "neurosymbolic programming" -- the Scallop project from Mayur Naik's group is particularly exciting to me), or finding ways to use PL techniques to solve ML problems. For an example of the latter, I just flipped through this year's PLDI papers, and one caught my eye that sounds like it has nothing to do with AI, "Hashing Modulo Context-Sensitive Alpha Equivalence." (Decoding the jargon, that means "How to deal with an enormous set of programs that contain lambdas" -- something that comes up when doing search-based synthesis and superoptimization.) Its abstract ends: "We have employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes." I think PL techniques do provide the key to overcoming a lot of the problems with LLMs. You want your LLM to have better correctness, reasoning, and goal-directed search -- researchers in programming languages and formal methods are expert at this. I am here to some extent conflating PL/FM techniques with traditional automated reasoning, but I think that's a fine conflation to make, because such techniques have been incubated by the PL/FM communities for the past 30 years since they were sidelined by AI. Case in point: very large fraction of computational logic and automated reasoning papers are motivated by problems in program analysis, verification, and synthesis.. https://easychair.org/smart-program/FLoC2022/index.html https://easychair.org/smart-program/FLoC2022/index.html As for what I have been up to: Trained a few hundred more software engineers, mirdin.com . While I mostly stayed away from AI stuff during my Ph. D., I've given in to the tides, and am now building a startup using my AI, PL, and pedagogy expertise to solve all problems related to codebase-learning (onboarding new hires, changing teams faster, etc). At the very end of my Ph. D., I discovered a new program synthesis technique based on constrained tree automata, and used it to build a synthesizer which is 8x more performant on one benchmark than the previous SOTA while using 10x less code. https://www.jameskoppel.com/files/papers/ecta.pdf https://www.jameskoppel.com/files/papers/ecta.pdf . So the research I've done since graduating has largely been follow-ups to that. See https://www.computer.org/csdl/proceedings-article/icst/2023/566600a293/1NsXOaMsvja https://www.computer.org/csdl/proceedings-article/icst/2023/... , https://pldi22.sigplan.org/details/egraphs-2022-papers/4/E-Graphs-VSAs-and-Tree-Automata-a-Rosetta-Stone https://pldi22.sigplan.org/details/egraphs-2022-papers/4/E-G... . I'm currently on two collaborations. One is continuing to develop algorithms for new kinds of constrained tree automata that can synthesize more kinds of programs. The other is an outgrowth of my startup: an empirical study on existing tools for codebase learning. Anyway, that's not a comprehensive answer on what to watch out for in the field, which I am not presently qualified to give if I ever was, but it's the things that have my attention. Oh, but: watch Isil Dillig. Everything that comes out of her lab is good.
  - squircle 2y ago
    Thank you for your thoughtful reply @Darmani. Best of luck with your current and future endeavors!
bbor 2y ago
Thanks for offering your time! 1. How do you/y'all feel about the ethics of publishing this kind of detailed instructional material for self-replicating machines on the open internet, given the potential risk of behavioral singularities from as-of-yet-uncharted intelligence explosion dynamics? I mean this question in the most friendly, least “gotcha” way possible — feel free to answer flippantly! 2. What would you say was the “frame problem” of this work that blocked progress, either recently or in your historical readings? I’m just starting to examine this literature after intentionally not engaging while designing my own systems, and it seems pretty damn robust in a post-frame-problem world. What might I be missing out of naïveté?
- Darmani 2y ago
  1. I've been a doomer since before the term was invented, and I never had any worry about synthesis research based on symbolic techniques. Gödel is our friend here: they're not powerful enough to model themselves. The best you get is stuff like https://ieeexplore.ieee.org/abstract/document/7886678?casa_token=XcQTz0HnqJcAAAAA:U9YCIDopCla_slF3fHzJwjPPf_UsRRVJ25DDhyuWlaIfYZbldPi2TQFhpMhLGXg5Up2YMLTE https://ieeexplore.ieee.org/abstract/document/7886678?casa_t... . An important component of the Sketch synthesizer is its simplifier, and this paper used Sketch to synthesize a better simplifier, and that speeds up synthesis times by 15%-60%. But that's a one-time improvement. The exponential take off comes from somewhere else. 2. Let me see if I understand your question: I think you're saying "The frame problem of AI and philosophy, https://plato.stanford.edu/entries/frame-problem/ https://plato.stanford.edu/entries/frame-problem/ , was the major blocker in AI systems, and now it's been solved by deep learning. What is the corresponding problem in program synthesis?" I think your "pretty damn robust" comment is important, but haven't yet figured out what you mean. Part of the reason I found this confusing is that the literal frame problem also appears in PL and synthesis, primarily in the verification of heap-based imperative programs. See the "frame rule" of separation logic. So anyway, what do I see as the big challenges stopping synthesis from reaching its dream of being able to generate well-designed large programs with little input? My two answers: First, there's the problem of finding good abstractions. You see this in very old work:trying to prove an imperative program works is easy to automate EXCEPT for the problem of finding loop invariants. This has remained a challenging problem in the 50 years since it was first described. Craig interpolation is the classic solution, but it only goes so far. The synthesis view is: figuring out how to write loops is not straightforward because you need to summarize infinitely possible states. And that's loops; designing data structures and finding good invariants for stateful applications is harder still. Second is what I like to call the "semantic veil." Generally, for any given chunk of code, there are multiple goals and abstractions that yield the same chunk of code. See my analogy to dairy-free chocolate chips in https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html https://www.pathsensitive.com/2023/03/modules-matter-most-fo... . So deducing the intentions of a piece of code from just the code itself is literally impossible. Unfortunately, the way humans design programs is much better understood as being about these higher-level organizational structures, and not about the code itself. This is an area where I'm excited about the potential of LLMs: they can make excellent use of the information in priors and in natural language to guess said intentions.
sgt101 2y ago
OK! I work in financial services, a lot of customers want tools to support their creaking code bases. What are the state of the art options, both commercial and open source? What are the prospects for things like translating COBOL to Python or Java?
- Darmani 2y ago
  Supporting an old codebase is a pretty broad question. There are quite a few companies supporting COBOL. But for migrations, and really anything interesting or unique, I recommend Semantic Designs. http://www.semdesigns.com/ http://www.semdesigns.com/ . Past customers include ADP, the Social Security Administration, the Bank of Australia/New Zealand, and Goldman Sachs Australia. They do everything, but COBOL migrations are their bread-and-butter. There are hundreds of COBOL dialects out there, and they have no trouble supporting all of them. I did interned for them in 2016, and the CEO served on my thesis committee. But I'm not saying this because I worked there; I worked there because I thought they had the best tech.
  - sgt101 2y ago
    This is super interesting, thank you. But, looking at semdesign's site and info I have a question - which is if this tech exists since 2010 or so... why are all the big banks not using it? Is it just bad marketing or is there a gotcha? They are all whining about their cobol problem, this could be a fix...... Does this mean that the market is not what folks imagine?
    - Darmani 2y ago
      Oh, some of the big banks are. But: Au contraire. It's existed much longer than that. So you've heard of products called vitamins and painkillers? The CEO of Semantic Designs, Ira Baxter, calls the kinds of migrations and mass changes they sell "heart surgery." As in: "How many people go to the doctor and say 'Doctor, I think I need some heart surgery?' No one." A very common thing that happens is that a company starts a project to upgrade some dying system and gets cold feet in the middle and then scraps the project. "We survived last year, we're surviving this year, we'll survive next year." Sometimes it takes extreme pressure, like the compiler for the original language no longer existing, before they migrate. (And it's not just the really big changes. A friend of mine, who founded another program-transformation startup, discovered this when he landed a deal using his tool to upgrade some company from PHP 4 to PHP 5. They decided that they needed way more code review than the kinds of trivial changes being made actually should require, decided not to do it, and then wound up not doing the upgrade.) When Ira begins talking to a new customer, he asks two questions: 1. How long have you been in your job? 2. Have you tried to do this kind of thing before? If the answer to #1 is too long, then he knows that either the manager he's talking too is risk-averse and complacent, or that he'll be promoted to his next job in the middle of the project. To make a good deal, he needs his counterpart to be someone who wants this kind of upgrade to be their big initiative that will help them rise. If the answer to #2 is no, then he'll know that eventually talks will break down and then they'll try to do it manually or in-house by underestimating how hard it is. For their most famous project, the B-2 Stealth Bomber migration, Northrop Grumman did exactly that -- came to Semantic Designs after a failed manual migration and a failed in-house tool development effort. So, yeah -- it's a very tough market. The buyers don't behave like you think they should. I wrote about this some in an appendix to pathsensitive.com/2023/09/its-time-for-painkillers-vitamins-die.html
algo_trader 2y ago
For practical systems, do you think improving the compiler toolchain is a good direction ? For example, speeding up compilation of 100s of similar code candidates, doing the same for eval, etc
- Darmani 2y ago
  That's very relevant to generate-and-test program search. The SBSE (search-based software engineering) and APR (automated program repair) communities do that kind of stuff. E.g.: There's a paper from that world, which I can't presently find, on "super mutants": basically, use environmental variables as feature flags so that you can compile 100 variants at once. Back when I worked in this space, one of the best things I did was run the Java compiler from within nailgun (program that saves JVM startup time) to compile mutants faster. Symbolic program synthesis doesn't work like this. They effectively has its own compiler toolchain that transform programs into constraint systems and/or do partial evaluation of programs with wholes. Most of them never run a traditional compiler; they just guarantee that they output correct code.

Hi @Darmami, what have you been working on in the meanwhile? Given the current state of programming and compsci research, what interests you these days? (What do you see as most important 5 to 10 years down the road?) As a layperson I don't have time to grok most of this but revisit from time to time.

Darmani 2y ago
Hi Squircle! I mostly left academia after graduating, and am not actively following current research, although I still live in Cambridge and attend a fair number of research events. I can say that deep learning has taken over PL research, just like everything else. A good number of PL and synthesis people have shifted heavily into pure deep learning, and a large proportion of those that haven't are working either on applying deep learning and LLMs to solve PL problems, fusing PL and ML techniques (aka "neurosymbolic programming" -- the Scallop project from Mayur Naik's group is particularly exciting to me), or finding ways to use PL techniques to solve ML problems. For an example of the latter, I just flipped through this year's PLDI papers, and one caught my eye that sounds like it has nothing to do with AI, "Hashing Modulo Context-Sensitive Alpha Equivalence." (Decoding the jargon, that means "How to deal with an enormous set of programs that contain lambdas" -- something that comes up when doing search-based synthesis and superoptimization.) Its abstract ends: "We have employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes." I think PL techniques do provide the key to overcoming a lot of the problems with LLMs. You want your LLM to have better correctness, reasoning, and goal-directed search -- researchers in programming languages and formal methods are expert at this. I am here to some extent conflating PL/FM techniques with traditional automated reasoning, but I think that's a fine conflation to make, because such techniques have been incubated by the PL/FM communities for the past 30 years since they were sidelined by AI. Case in point: very large fraction of computational logic and automated reasoning papers are motivated by problems in program analysis, verification, and synthesis.. https://easychair.org/smart-program/FLoC2022/index.html https://easychair.org/smart-program/FLoC2022/index.html As for what I have been up to: Trained a few hundred more software engineers, mirdin.com . While I mostly stayed away from AI stuff during my Ph. D., I've given in to the tides, and am now building a startup using my AI, PL, and pedagogy expertise to solve all problems related to codebase-learning (onboarding new hires, changing teams faster, etc). At the very end of my Ph. D., I discovered a new program synthesis technique based on constrained tree automata, and used it to build a synthesizer which is 8x more performant on one benchmark than the previous SOTA while using 10x less code. https://www.jameskoppel.com/files/papers/ecta.pdf https://www.jameskoppel.com/files/papers/ecta.pdf . So the research I've done since graduating has largely been follow-ups to that. See https://www.computer.org/csdl/proceedings-article/icst/2023/566600a293/1NsXOaMsvja https://www.computer.org/csdl/proceedings-article/icst/2023/... , https://pldi22.sigplan.org/details/egraphs-2022-papers/4/E-Graphs-VSAs-and-Tree-Automata-a-Rosetta-Stone https://pldi22.sigplan.org/details/egraphs-2022-papers/4/E-G... . I'm currently on two collaborations. One is continuing to develop algorithms for new kinds of constrained tree automata that can synthesize more kinds of programs. The other is an outgrowth of my startup: an empirical study on existing tools for codebase learning. Anyway, that's not a comprehensive answer on what to watch out for in the field, which I am not presently qualified to give if I ever was, but it's the things that have my attention. Oh, but: watch Isil Dillig. Everything that comes out of her lab is good.
- squircle 2y ago
  Thank you for your thoughtful reply @Darmani. Best of luck with your current and future endeavors!

bbor 2y ago

Thanks for offering your time! 1. How do you/y'all feel about the ethics of publishing this kind of detailed instructional material for self-replicating machines on the open internet, given the potential risk of behavioral singularities from as-of-yet-uncharted intelligence explosion dynamics? I mean this question in the most friendly, least “gotcha” way possible — feel free to answer flippantly! 2. What would you say was the “frame problem” of this work that blocked progress, either recently or in your historical readings? I’m just starting to examine this literature after intentionally not engaging while designing my own systems, and it seems pretty damn robust in a post-frame-problem world. What might I be missing out of naïveté?

Darmani 2y ago
1. I've been a doomer since before the term was invented, and I never had any worry about synthesis research based on symbolic techniques. Gödel is our friend here: they're not powerful enough to model themselves. The best you get is stuff like https://ieeexplore.ieee.org/abstract/document/7886678?casa_token=XcQTz0HnqJcAAAAA:U9YCIDopCla_slF3fHzJwjPPf_UsRRVJ25DDhyuWlaIfYZbldPi2TQFhpMhLGXg5Up2YMLTE https://ieeexplore.ieee.org/abstract/document/7886678?casa_t... . An important component of the Sketch synthesizer is its simplifier, and this paper used Sketch to synthesize a better simplifier, and that speeds up synthesis times by 15%-60%. But that's a one-time improvement. The exponential take off comes from somewhere else. 2. Let me see if I understand your question: I think you're saying "The frame problem of AI and philosophy, https://plato.stanford.edu/entries/frame-problem/ https://plato.stanford.edu/entries/frame-problem/ , was the major blocker in AI systems, and now it's been solved by deep learning. What is the corresponding problem in program synthesis?" I think your "pretty damn robust" comment is important, but haven't yet figured out what you mean. Part of the reason I found this confusing is that the literal frame problem also appears in PL and synthesis, primarily in the verification of heap-based imperative programs. See the "frame rule" of separation logic. So anyway, what do I see as the big challenges stopping synthesis from reaching its dream of being able to generate well-designed large programs with little input? My two answers: First, there's the problem of finding good abstractions. You see this in very old work:trying to prove an imperative program works is easy to automate EXCEPT for the problem of finding loop invariants. This has remained a challenging problem in the 50 years since it was first described. Craig interpolation is the classic solution, but it only goes so far. The synthesis view is: figuring out how to write loops is not straightforward because you need to summarize infinitely possible states. And that's loops; designing data structures and finding good invariants for stateful applications is harder still. Second is what I like to call the "semantic veil." Generally, for any given chunk of code, there are multiple goals and abstractions that yield the same chunk of code. See my analogy to dairy-free chocolate chips in https://www.pathsensitive.com/2023/03/modules-matter-most-for-masses.html https://www.pathsensitive.com/2023/03/modules-matter-most-fo... . So deducing the intentions of a piece of code from just the code itself is literally impossible. Unfortunately, the way humans design programs is much better understood as being about these higher-level organizational structures, and not about the code itself. This is an area where I'm excited about the potential of LLMs: they can make excellent use of the information in priors and in natural language to guess said intentions.

sgt101 2y ago

OK! I work in financial services, a lot of customers want tools to support their creaking code bases. What are the state of the art options, both commercial and open source? What are the prospects for things like translating COBOL to Python or Java?

Darmani 2y ago
Supporting an old codebase is a pretty broad question. There are quite a few companies supporting COBOL. But for migrations, and really anything interesting or unique, I recommend Semantic Designs. http://www.semdesigns.com/ http://www.semdesigns.com/ . Past customers include ADP, the Social Security Administration, the Bank of Australia/New Zealand, and Goldman Sachs Australia. They do everything, but COBOL migrations are their bread-and-butter. There are hundreds of COBOL dialects out there, and they have no trouble supporting all of them. I did interned for them in 2016, and the CEO served on my thesis committee. But I'm not saying this because I worked there; I worked there because I thought they had the best tech.
- sgt101 2y ago
  This is super interesting, thank you. But, looking at semdesign's site and info I have a question - which is if this tech exists since 2010 or so... why are all the big banks not using it? Is it just bad marketing or is there a gotcha? They are all whining about their cobol problem, this could be a fix...... Does this mean that the market is not what folks imagine?
  - Darmani 2y ago
    Oh, some of the big banks are. But: Au contraire. It's existed much longer than that. So you've heard of products called vitamins and painkillers? The CEO of Semantic Designs, Ira Baxter, calls the kinds of migrations and mass changes they sell "heart surgery." As in: "How many people go to the doctor and say 'Doctor, I think I need some heart surgery?' No one." A very common thing that happens is that a company starts a project to upgrade some dying system and gets cold feet in the middle and then scraps the project. "We survived last year, we're surviving this year, we'll survive next year." Sometimes it takes extreme pressure, like the compiler for the original language no longer existing, before they migrate. (And it's not just the really big changes. A friend of mine, who founded another program-transformation startup, discovered this when he landed a deal using his tool to upgrade some company from PHP 4 to PHP 5. They decided that they needed way more code review than the kinds of trivial changes being made actually should require, decided not to do it, and then wound up not doing the upgrade.) When Ira begins talking to a new customer, he asks two questions: 1. How long have you been in your job? 2. Have you tried to do this kind of thing before? If the answer to #1 is too long, then he knows that either the manager he's talking too is risk-averse and complacent, or that he'll be promoted to his next job in the middle of the project. To make a good deal, he needs his counterpart to be someone who wants this kind of upgrade to be their big initiative that will help them rise. If the answer to #2 is no, then he'll know that eventually talks will break down and then they'll try to do it manually or in-house by underestimating how hard it is. For their most famous project, the B-2 Stealth Bomber migration, Northrop Grumman did exactly that -- came to Semantic Designs after a failed manual migration and a failed in-house tool development effort. So, yeah -- it's a very tough market. The buyers don't behave like you think they should. I wrote about this some in an appendix to pathsensitive.com/2023/09/its-time-for-painkillers-vitamins-die.html

algo_trader 2y ago

For practical systems, do you think improving the compiler toolchain is a good direction ? For example, speeding up compilation of 100s of similar code candidates, doing the same for eval, etc

Darmani 2y ago
That's very relevant to generate-and-test program search. The SBSE (search-based software engineering) and APR (automated program repair) communities do that kind of stuff. E.g.: There's a paper from that world, which I can't presently find, on "super mutants": basically, use environmental variables as feature flags so that you can compile 100 variants at once. Back when I worked in this space, one of the best things I did was run the Java compiler from within nailgun (program that saves JVM startup time) to compile mutants faster. Symbolic program synthesis doesn't work like this. They effectively has its own compiler toolchain that transform programs into constraint systems and/or do partial evaluation of programs with wholes. Most of them never run a traditional compiler; they just guarantee that they output correct code.