Where are we going from here? Software engineering needs formal methods • Hacker News Board

Re: Where are we going from here? Software engineering needs formal methods

#101

Post by nivertech » Sun, Jul 04, 2021, 8:35 AM UTC

stan_rogers wrote: post #49

ironman1478 wrote: post #39

Earlier quoted context omitted.

How do you know it's working if it doesn't have unit tests that exercise edge cases? Or even basic functionality? Also, good unit testing can allow you to reduce the time it takes to write software by giving you an isolated environment to run your code. Unit tests are a tool to get you to working code.

No. Failed tests can only tell you that you've found a problem; passed tests can't tell you there aren't any problems present. Provably correct code can be proven correct.

> Provably correct code can be proven correct.

there are two different types of formal proofs:

1. there is at least one error in the code, or

2. there are no errors at all

The [1] is much easier than [2].

Re: Where are we going from here? Software engineering needs formal methods

#102

Post by cryptos » Sun, Jul 04, 2021, 8:44 AM UTC

I think a sweet spot is "specification by example" also called behavior driven development (BDD). You take a more or less standardized, but human readable language to write down the specification and implement test adapters for it.

A typical tool for this approach would be Cucumber: https://cucumber.io/

Re: Where are we going from here? Software engineering needs formal methods

#103

Post by cloogshicer » Sun, Jul 04, 2021, 9:32 AM UTC

cryptos wrote: post #102

I think a sweet spot is "specification by example" also called behavior driven development (BDD). You take a more or less standardized, but human readable language to write down the specification and implement test adapters for it. A typical tool for this approach would be Cucumber: https://cucumber.io/

Having done BDD at work, I can only say it's not the right approach.

The "human-readableness" of the test cases produced with BDD is debatable - at least at our company only technical people familiar with the code could understand the spec.

At the same time BDD was very cumbersome to do, while not really providing us any benefits.

Re: Where are we going from here? Software engineering needs formal methods

#104

Post by nicoburns » Sun, Jul 04, 2021, 9:55 AM UTC

tsimionescu wrote: post #96

SkyMarshal wrote: post #95

Earlier quoted context omitted.

>but I’m not sure a CRUD app will. Considering most corporate websites are CRUD apps, and they keep getting pwned via some bug or vulnerability and millions of private user information stolen and pawned off in the black market, I don't think that's an assumption we can make anymore. That said, full-on formal methods may still be overkill. A web framework built in a language with a strong type system and input sanitat…

I'm not sure type safety is the right key here. Rather, better defaults in web and SQL frameworks, even in a dynamic language, would get you most of the way there. You can even use dynamic types to mandate that input is sanitized - a crash is much louder than SQL injection or XSS.

> You can even use dynamic types to mandate that input is sanitized

If you're using types to mandate that input is santized, then that sounds like type safety to me!

Re: Where are we going from here? Software engineering needs formal methods

#105

Post by ud_0 » Sun, Jul 04, 2021, 10:12 AM UTC

In my opinion, formal methods for software engineering have been heavily advocated for by people and organizations who want to sell books, seminars, and conferences. People who want to act as gatekeepers while extracting money from the system and reframe history in their own terms.

That's not to say formal methods are bad per se, there is just a lot of reason to doubt motives and outcomes behind concerted overarching initiatives.

The notion that software engineering should be grouped under civil engineering is misguided. Part of the reason why we're looking to other fields is to profit from their experience (which is good) but part of it is also because we're desiring a kind of legitimacy we feel is absent. It's a reasonable impulse to a degree, for smart people dedicating their productive years to a discipline. We want to do a good job.

The problem is that we have more in common with architects than we do with civil engineers. There are some goals that can be measured with a boolean outcome: does the code compile, is a certain algorithm provably correct given certain conditions, can a building be built. But it gets murky very very quickly: how well does a thing we create serve its purpose? Does it use resources efficiently? How long will a structure last? What kind of adverse conditions will bring it down? Does the thing make people's lives better and if so by what measure? These are a small hint at the questions where formal methods tend to fall down or even work against us.

So do we need overarching formal methods or do we need to be more scientific about specific objectives and measurement of outcomes that are important to us subjectively?

Re: Where are we going from here? Software engineering needs formal methods

#106

Post by pjmlp » Sun, Jul 04, 2021, 10:29 AM UTC

Very unwelcome opinion around here.

We could start by stop calling software engineering to 6 months coding bootcamps, letting it for actual 5 years experience being taught correct engineering practices and respective skill assessment.

Then we can start talking about adopting what is still missing from real engineering practices into the field.

Ah, and in the process make companies liable for skipping quality control when everything goes wrong.

Re: Where are we going from here? Software engineering needs formal methods

#107

Post by skneko » Sun, Jul 04, 2021, 10:42 AM UTC

I am a research intern working in a group studying and developing formal methods. The tech we are working with has served to verify planes, trains and has been used in NASA. AMA if anyone here is curious about how the world around FM works.

Re: Where are we going from here? Software engineering needs formal methods

#108

Post by rhizome » Sun, Jul 04, 2021, 11:03 AM UTC

werpon wrote: post #4

Formal methods may work for civil engineering where the usual workflow is gathering requirements, developing a detailed project and building the thing, with the implicit understanding that any little change will mean recalculating costs and deadlines. When your customer decides to pivot the fintech app you were developing into a cryptocurrency investment tool, it makes no sense.

Formal methods come from a need for form, repeatability. There is nothing in software development that comes close to the process and considerations that go into choosing to build with M30 concrete, or use #5 rebar for that matter.

Re: Where are we going from here? Software engineering needs formal methods

#109

Post by tluyben2 » Sun, Jul 04, 2021, 11:04 AM UTC

hintymad wrote: post #24

It really depends on the project, or put it another way, the ROI. Then core protocols of a storage system or an OS kernel will benefit from formal methods, but I’m not sure a CRUD app will. Besides, TLA+ is not panacea in formal methods. It’s a specification language, which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concepts, such as spur…

> Not that people are incapable

I think that is quite an overestimation of what most people in the industry can do.

Re: Where are we going from here? Software engineering needs formal methods

#110

Post by Taek » Sun, Jul 04, 2021, 11:07 AM UTC

ud_0 wrote: post #105

In my opinion, formal methods for software engineering have been heavily advocated for by people and organizations who want to sell books, seminars, and conferences. People who want to act as gatekeepers while extracting money from the system and reframe history in their own terms. That's not to say formal methods are bad per se, there is just a lot of reason to doubt motives and outcomes behind concerted overarching…

I think it depends on what you are building. For example, if you are building a database that houses user data and user credentials, this is is a very well understood thing that experienced professionals can set up quickly, efficiently, and give you both a lot of security and also enough flexibility to build whatever business you want behind it.

And yet, it seems that most companies and websites that handle user credentials do a poor job at it. So there does seem to be an argument in favor of adding formal methods in certain areas of software design and engineering.

One thing that very much distinguishes the software world from every other type of engineering is the complexity and rate of innovation. In software, I can invent and deploy a thing on the same day and the total R&D cost to my company is almost exactly equal to my salary for that day. Whereas for something like a bridge, the R&D cycle for a new bridge invention could be several months and hundreds of thousands of dollars for a similar idea.

Overall, I think the discussion about putting standards in place for certain common activities (network communications, password databases, encryption standards, and similarly well understood areas) is worth having. Though I also would be concerned that state actors would use such standardization to insert weaponized requirements like backdoors, or that regulation would prevent new innovations from gaining a foothold.