saurabh20n

13 ms·

61.
by saurabh20n 8y ago
Trail of bits is not building anything in program synthesis.
62.
by saurabh20n 8y ago
About the benchmarks, SMT-LIB has had my instances for close to a decade now :) [1,2] We are now generating non-bitvector benchmarks, and maybe in the Fall we will submit newer instances. Back in the day, I was foolish enough to implement m
63.
by saurabh20n 8y ago
The below were written for a semi- or non-technical audience, and only address your curiosity tangentially, but better than nothing: * Program synthesis overview: https://medium.com/@vidiborskiy/software-writes-software
64.
by saurabh20n 8y ago
Z3 is amazing. I have been working with it since 2007. We are now building program synthesizers using it. Having a solid system to do the heavy lifting is a life saver.
65.
by saurabh20n 8y ago
Agree with the scale. But do you mean the compilers toolchain is the largest/safest; or the overall C++ codebase. No questions about the latter, but would be surprised if you meant the former. Out of curiosity: if not the language plat
66.
by saurabh20n 8y ago
Honest question: does the current Google have the environment to innovate on the next generation of compilers/PL/program synthesizers? I would have definitely said yes back in the day; but not so sure now. (Admittedly might be bia
67.
by saurabh20n 8y ago
Synthetic Minds (YC S18) | SF + Seattle | $120k+ | First 5 engineers: commensurate equity | ONSITE, Full Time The ideal candidate has a master/phd in systems, compilers, programming languages, or distributed systems; but never gets to
68.
by saurabh20n 8y ago
As some other people have pointed out, you have to pick the domain and application. Airbus controllers (abstract interpretation [1]), Microsoft software driver verification (SLAM model checker [2]) were ones where formal methods found use i
69.
by saurabh20n 8y ago
90% of the page at the bottom is the transcript. Right below the audio file is the time annotated transcript as well. Might have been added after you opened it: should recheck.
70.
Stereoscopic Images of Ultima Thule from New Horizons(wired.com)
4 points by saurabh20n 8y ago|0 comments
71.
Incredible videos of SpaceX's failed landing(wired.com)
2 points by saurabh20n 8y ago|1 comments
72.
NASA Insight is on Mars(twitter.com)
72 points by saurabh20n 8y ago|3 comments
73.
by saurabh20n 8y ago
It would be useful to have a section: "What AI cannot do" or to be pedantic: "What the current AI techniques cannot do."
74.
by saurabh20n 8y ago
Comparison-based sorts have O(1) complexity on the size of the elements being sorted. I.e., comparison between two numbers is a single instruction assuming numbers fit within a word. Even if you assume very very large numbers then compariso
75.
by saurabh20n 8y ago
Synthetic Minds (YC S'18) | mostly ONSITE in SF | First non-founder engineers We're building program synthesizers, i.e., automation that can write code. I have an MVP in production that reads/writes smart contracts (i.e., sma
76.
by saurabh20n 8y ago
I'm guessing you meant McAfee for Dapps? Yes. It should work. There's a good amount of work to be done though. :) I don't follow what you mean by a "debugger" in this case.
77.
by saurabh20n 8y ago
Ah. I see why that was unclear. I make multiple SMT queries. SMT solvers work well in practice, but they are solving a problem which is between NP-Complete to Undecidable (when quantifiers are involved [1]). Also, we are using a very hand-w
78.
by saurabh20n 8y ago
Thanks! The key distinction is building a synthesizer, not just a verifier. These systems are hard to use, and synthesized code is the key to making them accessible. Watch the demo videos. See if you agree. On the verifier side: QSP is a pr
79.
by saurabh20n 8y ago
You sir or madam, have a devious mind :). I shall hold on to my trust in humanity for a little while longer!
80.
by saurabh20n 8y ago
If you see the demo runs on the website FAQ, that example of about 20-50 LoC cost ~$200. You can extrapolate accordingly. Now if you integrate into your CI, I am of course going to only rerun on changes (syntactic, easily checked; and hopef
81.
by saurabh20n 8y ago
Fixed. Thanks for noticing.
82.
by saurabh20n 8y ago
Look up Nate's work [1], specifically Boomerang [2] that aims for bidirectional programming. Be crazy :) [1] Nate Foster: http://www.cs.cornell.edu/~jnfoster/ [2] Boomerang http://www.seas.upenn.edu&#x2
83.
by saurabh20n 8y ago
It will be pay for use, like AWS. You fill up, and then depending on how compute-heavy your contracts are to analyze, you will be charged accordingly. Your costs will end up depending on complexity of your contracts. Compare this to the alt
84.
by saurabh20n 8y ago
Your `D(K(..))` notation is better than mine. Email me, and I will send you a gift card. What you do is solve `\exists D: \forall arr: D(K(arr)) = arr` where `arr` is an arbitrary length array/bitstream. See paper [1]. There is also re
85.
by saurabh20n 8y ago
I get your concern about the current-state . The "dev/money" ratio needs adjustment. Market cap/ICO/yet-another-cryptocurrency is not what excites me. I am working on a simple premise: The DAO (perpetually running,
86.
by saurabh20n 8y ago
Yes. The hope is that you run this analysis as part of your development workflow. e.g., on every merge into master. Charge up like AWS and use as frequently as you need. The current alternatives involve hiring a firm for $20-500k for a manu
87.
by saurabh20n 8y ago
All great points. And I agree with you on most everything. I care about the major complicated projects succeeding, e.g., 0x, Golem, Augur, Aragon, to name a few. They can go the DAO route, or I can do my part in helping. Help me get in touc
88.
by saurabh20n 8y ago
LOL. I agree. Want to take a stab at it?
89.
by saurabh20n 8y ago
I am not using Rosette, although I love the work Emina and Ras are doing to make synthesis accessible. [ Edit: Your idea is fantastic, btw. If you can find use cases where the size of contracts is small, it'll be amazing to have synthe
90.
by saurabh20n 8y ago
Absolutely right! Which is why I am connecting directly with the project developers. Also, I specifically built it to run over Solidity source code. As opposed to EVM bytecode like other tools. Only 1% of contracts have their Solidity code

More ›