Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: Symbolica – Try our symbolic code executor in the browser

news.ycombinator.com

Post reply on HN
Print view View original

1–10 of 37 posts

Show HN: Symbolica – Try our symbolic code executor in the browser

#1

Post by Choc13 »

We're a couple of software engineers who believe that to build great software you need to write good tests, but we also sympathise when engineers say things like:

- "Writing tests was too time consuming on my tight schedule", or

- "Unit tests don't catch enough bugs, so they're useless", or

- "I've inherited a legacy code base without tests and have no idea where to start"

To tackle this we're building Symbolica (https://www.symbolica.dev), a symbolic code executor [1], that lets you run your code for all possible inputs. This means you can do things like:

- Assert properties about your code and check that they hold for every conceivable input.

- Check that two implementations of the same function/method/program are equivalent, which is really useful if you're refactoring a legacy codebase without tests.

- Find out if your code will hit any undefined behaviours, e.g. divide by zero or out of bounds array access.

We're still really early in the development of this product, but we're excited to have built a working prototype of the symbolic executor for C programs. We wanted to get some feedback from potential early adopters so we've put up a code playground (https://www.symbolica.dev/playground) where you can try out Symbolica on C programs in the browser for free. We'd love people to give it a go and give us their thoughts.

Our plan is to build this out into a hosted cloud service that you can integrate into your DevOps pipeline (e.g. GitHub actions) so that you can run these symbolic tests on every CI build.

Further down the line we plan to add support for other languages too. We've currently got proof of concept implementations for Lisp and Python and will be looking into C++, Rust and .NET after. Of course we're always willing to prioritise a particular language if there's strong demand.

If you're interested in what we're building then please either message us at dev@symbolica.dev or join the alpha waiting list if you want to get first access to our full offering once we launch that.

For those curious about how the executor works the core part of it is open source on GitHub (https://github.com/SymbolicaDev/Symbolica)

[1] https://en.wikipedia.org/wiki/Symbolic\_execution

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#3

Post by brudgers »

Link, https://www.symbolica.dev

I tried the try for free button.

The run took longer than my attention span. Since I'm not a potential customer, that's not a data point.

On the other hand, adding some text to the code editor page quantifying in minutes and seconds how long running example code will take would be a low effort way to manage user expectations.

Setting the context as a proof of concept is ok. It's honest. Letting people know it will be slow is good because it is honest, too.

Give people evidence that you can be trusted. Javascript that runs on back-button mouse over is not where to put your efforts. Good luck.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#4

Post by Choc13 »

brudgers wrote: post #3

Link, https://www.symbolica.dev I tried the try for free button. The run took longer than my attention span. Since I'm not a potential customer, that's not a data point. On the other hand, adding some text to the code editor page quantifying in minutes and seconds how long running example code will take would be a low effort way to manage user expectations. Setting the context as a proof of concept is ok. It's honest…

Thanks for the comments, they’re good points. I’ll update the page as you suggested as yeah right now at the PoC stage it’s on the slow side.

Some of the time lag is due to us waiting for the build stage to complete, which isn’t actually the core part of the product and is only required for the playground site. I’ll try and make this more explicit too so that people can get a sense for how long the actual symbolic execution part takes, which is the actual delta that will be added if they were to use it in their DevOps pipeline.

We also have some speed improvements to the executor that we’ll be shopping soon. We’ve tested locally but just need to port to the cloud version.

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#5

Post by Choc13 »

brudgers wrote: post #3

Link, https://www.symbolica.dev I tried the try for free button. The run took longer than my attention span. Since I'm not a potential customer, that's not a data point. On the other hand, adding some text to the code editor page quantifying in minutes and seconds how long running example code will take would be a low effort way to manage user expectations. Setting the context as a proof of concept is ok. It's honest…

I’m not quite sure what you meant by this statement

“Javascript that runs on back-button mouse over is not where to put your efforts.”

Was this something you observed on our site, or just a general point about prioritising the core product over fancy UI effects on the website? Would you mind clarifying?

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#9

Post by pag »

Can you explain how your offering compares with open-source alternatives, such as KLEE [1] and DeepState [2]?

P.S. your logo is surprisingly similar to that of ForAllSecure [3], which also provides a symbolic execution engine called Mayhem [4].

[1] https://klee.github.io/ (online example: http://klee.doc.ic.ac.uk/)

[2] https://github.com/trailofbits/deepstate#readme

[3] https://forallsecure.com/

[4] https://users.ece.cmu.edu/~aavgerin/papers/mayhem-oakland-12...

Re: Show HN: Symbolica – Try our symbolic code executor in the browser

#10

Post by SebastianFish »

I think the problem this product is trying to solve, making it easier to implement rigorous testing, is an important one. When I talk to junior developers I compare enterprise software development to painting. When you paint a room, most of your time is actually spent taping out all of the edges and boundaries. The verb painting is a misnomer. Similarly, it isn't a fast or easy for devs to see all of the boundary conditions in inherited code bases and write meaningful tests for them.

You mention in the description about testing code for all possible inputs. Are you all actually doing this behind the scenes with an SMT solver? Are you using some other proof assistant (COQ, HOL, etc) to be able to use proof-by-induction techniques and thus manage the path explosion problem?

I tried out an example comparing two multiplication algorithms (see below) and the tool said it couldn't find any issues in about a minute. Curious whether it will scale to larger problem sizes.

// implementation 1 int mult(int x, int y) { return x*y; } // implementation 2 int slow_mult(int x, int y) { int result=0; if(x<0) { for(int i=x; i<0; i++) { result-=y; } } else { for(int i=0; i<x; i++) { result+=y; } } return result; }

Post reply on HN