3 ms·

This is a very backend/algorithm-centric view of correctness. What about user interfaces? What is a "correct" user interface? If a bug is "unexpected" behavior

This is a very backend/algorithm-centric view of correctness. What about user interfaces? What is a "correct" user interface? If a bug is "unexpected" behavior, and my user interface has several thousand users, how do I manage to not produce unexpected behavior to anybody? Many software supports workflows and processes in some enterprise, and those workflows shift subtly over time. How does Haskell help me write "correct" software in such a context, whatever that means? How do I deal with low quality of input data, when I can't ask my product owner to create a matrix of each case of missing data and behavior, because that would be exponential in size? Phrased another way, the problems with correctness that seem to trouble the author are not the problems with correctness that I tend to encounter often in my work. The case where there is a clear-cut bug in an algorithm tend to be easier to debug and fix than a bug that stems from several department having subtly different ideas of what certain pieces of data and action mean.

naringas 8y ago
https://www.hillelwayne.com/post/formally-specifying-uis/ https://www.hillelwayne.com/post/formally-specifying-uis/
Jtsummers 8y ago
A workflow can be modeled using something like a state machine or statecharts. That can be encoded into the type system in a language like Haskell. For front end stuff, you could model your system using something like [0] which uses statecharts. An example of unexpected behavior: Is it possible for a user of your application or site to end up in a state where the only next step is to close it and restart? Or can they properly navigate from nearly any display to any other? While the linked tool doesn't directly answer those questions, it will help you construct your models in a way that you can manually evaluate them more easily or convert to a TLA+ or similar specification and have the computer check that. Could you, or should you, use formal methods for everything? No. But it can be applied pretty broadly if you're open to it, and in fairly lightweight ways (especially these days since there's been a ton of interest over the last few years). Once you start recording your formal (or more formal) specs, you can also share them more easily. A major problem in coordinating with so many different groups is that they all have their own model for what's going on based on their interaction with the systems. By creating more formalized models that allow for clearer communication (a few statecharts versus pages and pages of prose; flow charts versus pseudocode) you can reduce the communication error between teams/departments. And with all the recent work going into it, and using more capable languages (or tools with less capable languages) you can encode much of this into your program and make correct system construction more feasible. [0] https://sketch.systems/ https://sketch.systems/
adrianmonk 8y ago
I thought they did a good job of acknowledging that with the section called "Correctness does not mean perfection". They're trying to treat that as an issue which is also valid but is separate, which made sense to me.

naringas 8y ago

https://www.hillelwayne.com/post/formally-specifying-uis/ https://www.hillelwayne.com/post/formally-specifying-uis/

Jtsummers 8y ago

A workflow can be modeled using something like a state machine or statecharts. That can be encoded into the type system in a language like Haskell. For front end stuff, you could model your system using something like [0] which uses statecharts. An example of unexpected behavior: Is it possible for a user of your application or site to end up in a state where the only next step is to close it and restart? Or can they properly navigate from nearly any display to any other? While the linked tool doesn't directly answer those questions, it will help you construct your models in a way that you can manually evaluate them more easily or convert to a TLA+ or similar specification and have the computer check that. Could you, or should you, use formal methods for everything? No. But it can be applied pretty broadly if you're open to it, and in fairly lightweight ways (especially these days since there's been a ton of interest over the last few years). Once you start recording your formal (or more formal) specs, you can also share them more easily. A major problem in coordinating with so many different groups is that they all have their own model for what's going on based on their interaction with the systems. By creating more formalized models that allow for clearer communication (a few statecharts versus pages and pages of prose; flow charts versus pseudocode) you can reduce the communication error between teams/departments. And with all the recent work going into it, and using more capable languages (or tools with less capable languages) you can encode much of this into your program and make correct system construction more feasible. [0] https://sketch.systems/ https://sketch.systems/

adrianmonk 8y ago

I thought they did a good job of acknowledging that with the section called "Correctness does not mean perfection". They're trying to treat that as an issue which is also valid but is separate, which made sense to me.