| ▲ | turbobutton 3 hours ago |
| I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world. Any software that's processing inputs and provides complex workflows to humans has to necessarily deal with the endless vagaries of reality. That's not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth... |
|
| ▲ | kodoman 2 hours ago | parent | next [-] |
| For me it seems more like modern software has built away from using formal mathematical models in the first place, not the necessarily the problem people want to solve have to have such a fuzzy definition of domain, but that the primitives of operating systems and software development have gone in the other direction. Think about the filesystem, the big issue with formalizing a program spec that operates on a file system is simply the fact it is essentially a shared object amongst all the programs running on the system. Add to that the fact that (though this changes with modern containerization systems, namespaces, pledge what ever) a program may at any point gain access to root permissions if it makes the system call to do so providing the correct credentials it becomes very difficult formally be able to remove any possible states from the system. All this could be different but we would radically need to redesign are systems and the way we think about the problems. |
| |
| ▲ | sigbottle 33 minutes ago | parent | next [-] | | Basic problems such as change over time and interoperability are reasons why formal methods break. Formal specification presumes a priori a great deal of control over the world in general, especially the more you move away "from nature" and more towards what a human might want to instantiate themselves. Formal methods often try not to deal with things they don't "understand", or try to abstract the parts that "don't matter" away. But inevitably it changes, and the repsonse to that change is to subsume more and more into your own ontology so you understand the nuances. Or you simply control all interoperable endpoints, and so the nuances vanish away, because you're in control. This is great when the battle is against nature. "Nature", for all its ambiguities, we generally can assume to be stable. What about with human society? In some sense, there might not be much to formal methods if you could solve the underlying capability of getting everybody to agree on the semantics in the first place, and have no desire for change at all. But that is an absurdly strong requirement. Formal methods is constantly a race to try and find good abstractions and then breaking them. I don't think there really is a way out of this, but I'm not that creative :/ | |
| ▲ | jcelerier 2 hours ago | parent | prev | next [-] | | Customer request: make a software that makes drawings that look good/my style/... Where do you start for formalizing this? | | |
| ▲ | hackingonempty an hour ago | parent | next [-] | | You start by defining a loss function. | |
| ▲ | yababa_y 2 hours ago | parent | prev | next [-] | | for example here was how some design rules got formalized into a checker during a video editing session of several hours: https://github.com/emberian/vidbox/blob/dev/render/drc.py | |
| ▲ | kodoman 2 hours ago | parent | prev | next [-] | | I mean would you take that spec as something you could deliver? This is not a real problem spec and is incredibly vague, but the first question would be around building a formal model for the drawing part of the application (and is the main aspect of the program) that might be easier then it first seems. There are various ways you could model the draw window depending on if it's a rasterizing program or a vector program either way not challenging, then formalize the operations of the program (various effects will necessary be well defined mathematical functions in the first place) and then prove what ever you feel you have to prove about the system. This is not to say it is easy or especially in this case you should even do it and my point was more about the system aspect of things or things that one would want to be able to reason about. An example of a spread sheet program might have been more productive example or a http API server or some kind of middle where program. I feel like you picked the most obtuse example possible even though my point was not to cover all possible programs that one might want to write. | | |
| ▲ | jcelerier an hour ago | parent | next [-] | | > I mean would you take that spec as something you could deliver? Yes, that's the kind of contract we take on regularly. My point is that the exact thing the customer wants/needs is the one part that can't be formalized meaningfully - it's good when we show them something and they tell us is good. Everything else doesn't matter - could be the worst UI, maybe you have to reboot the computer once before starting it and once after exiting it, maybe it leaks enough memory that you have to reboot every day anyways - what matters for them to pay you is "do they like the drawing quality" and really nothing else | | |
| ▲ | kodoman an hour ago | parent [-] | | I don't write these sort of programs but my thinking is that 'draw nice' is vague and I would not know what that means and indeed that is a fuzzy spec I would have only thought you needed more clarification on what good or nice here means and it sounds like what you do is actually work out most of what the program has to do and really they have asked you to make them a drawing program with them giving you input along the way. This indeed could not be formalized by it's very nature. I was not making a claim on the applicability or even the desirability for all programs and I think many people who have not look at it properly overestimate it's applicability. What I was trying to say is for the subset of programs that one would want to formalize (such as the examples I gave) the task could be much easier if we have formal primitives, including operating system primitives and networking primitives to provide guarantees. My other point would be that a lot of developers and projects are writing code that could potentially prove properties and benefits could be derived from proving these properties. I would look at middleware programs as some of the obvious ones that could massively benefit from such techniques and formalization (though things like streams can be much more easily formalized and modeled correctly). | | |
| ▲ | bluGill 36 minutes ago | parent [-] | | I don't write those sorts of programs either. There is evidence that some people do write that sort of program with varying amount of success in "draw nice". I'm sure such people could write books on what draw nice means. I would refuse such a job because I don't have the right expertise, and you probably wouldn't hire me for it even if I would accept it. However hire the right expert and you can probably get what you want even though at the start you don't even know what you really want - the other option is the expert will quickly realize is what you want is not what they can do and either tell you not to waste your money or warn you that you are going to spend a lot of money on an open ended research project that may or may not produce results. | | |
|
| |
| ▲ | bluGill an hour ago | parent | prev [-] | | That is very common for something given in the industry. It is our job as programmers to first figure out what the customer really wants, and then create enough of the requirements/spec to deliver it. That is one of the reasons for Agile vs Waterfall processes: nobody really knows what they want in the first place so you deliver something that you think is close and work with them to come up with something acceptable (acceptable covers both it does what they want, and also the cost to make it better). Any formal spec needs to be adjustable as we figure out requirements. OTOH, we can probably call a much less formal spec good enough. Just that it doesn't write past the end of buffers would be very helpful. We can also throw a bounds in - if we can't prove it in X iterations then call it false (expect to adjust X to very large) | | |
| ▲ | kodoman 36 minutes ago | parent [-] | | Not that vague first you need to know what the customer means by good. I was not making claims on the applicability of formal methods any way, only the point I was making about the primitives. |
|
| |
| ▲ | fultonn an hour ago | parent | prev [-] | | Inductively, in which case data labels are the spec and having good data is still the hardest part ;-) |
| |
| ▲ | ModernMech an hour ago | parent | prev [-] | | I don't think it has to be radically different... type systems are one example of formal models which languages have been moving towards recently. Especially with how they synergize with AI. Mainstream type systems are limited, but AI can use esoteric type systems with stronger guarantees, like capability permissions systems, which solve some of the issues you're highlighting. | | |
| ▲ | kodoman 38 minutes ago | parent [-] | | > type systems
Indeed types systems are usually the way formal verification is done, I am not denying that. The problem I am claiming is not the tools of formal verification but the domain one has to model and capture. What I was trying to show is the nightmare of modeling accurately and in a way that matters lots of operating system primitives and further reasoning about when the assumptions have been violated by the program set up. Indeed this does not effect the stuff outside the interaction of the program with the operating system and my point when it came to modern programming primitives is that not all data structures or methods of programming lend themselves to being able to write formal proofs about them. You might be able to have a type BigInterfaceTypeThatDoesLotsOfThings<a> but this might be impossible to formalize in any meaningful way and AI is not the panacea and this stuff is not easy and require hard thinking. Additionally a lot of formally verified programs are done via constructive proofs where you build up the correct program from primitives and extract the program and prove it that way. This requires generally requires a type system that has a complete inference algorithm like ML type-systems and are much harder to work with and you have to set up knowing you want to do this sort of thing. Capability systems indeed make a lot of sense for operating system level constraints and I agree this is a sensible direction and combined with type systems you can build some very powerful permission systems. But these do not solve formally verifying lots of behaviors and good capability system in my opinion (and something I worked on previous as a side project that is completely unfinished and abandoned.) need mathematical primitives and structures that lend themselves to proofs and being restricted by capabilities. Note capabilities become a program themselves and types can become programs, so getting your types right has the same issues in the first place when talking about this level of formalization. |
|
|
|
| ▲ | Groxx 3 minutes ago | parent | prev | next [-] |
| [delayed] |
|
| ▲ | an hour ago | parent | prev | next [-] |
| [deleted] |
|
| ▲ | tialaramex an hour ago | parent | prev | next [-] |
| > I believe there's a hard distinction between abstract, mathematical correctness in software and functioning in the real world. Sure, but people (perhaps including you) don't understand that it's foundational. That is, it's not enough to be correct, but if your program isn't even correct there's basically no chance it does what you intended. |
|
| ▲ | heresie-dabord an hour ago | parent | prev | next [-] |
| > not to say there isn't value in formal correctness, but the important part is identifying when it's useful and when its more trouble than its worth... We ought to be able to build high-confidence software. Unless you have bamboozled your customers completely, they should expect a product that you provide to be a) fit for purpose, b) fit for use, and c) secure. We know of course that very little commercial software is (d) proven correct. Software Correctness (d) is hard, no question. Just getting to ONE of { a, b, c } appears to be a bridge too far. But that's where professional rigour and diligence is required. btw good article, u/turbobutton. |
| |
| ▲ | godd2 an hour ago | parent [-] | | >We ought to be able to build high-confidence software. We are, it's just incredibly expensive. | | |
|
|
| ▲ | xpct 2 hours ago | parent | prev | next [-] |
| What I've learned this year is that we should be verifying the fridges.. |
| |
| ▲ | kodoman 2 hours ago | parent [-] | | Or thought more carefully about putting them on any LAN directly. | | |
|
|
| ▲ | darkwi11ow 3 hours ago | parent | prev | next [-] |
| I agree with you that for most software, verification was historically less of the requirement, however some software always needed to have abstract, mathematical correctness -- think military, medical, industrial automation. While these areas were main premise of an article when it was written, I think the
article really aged well into current time of mass AI/LLM deployment. It shows fundamental limitations of token based systems / symbolic reasoning that LLM espouses internally, while writing correct software. These limitations also apply to humans, however humans mental modelling, being not fully based on symbolic processing, have been historically shown capable of writing correct software systems, while AI/LLM systems have not been proven to be able to do that, and as article shows that with current token based technology it's unlikely they will ever be. |
| |
| ▲ | skydhash 3 hours ago | parent [-] | | > however some software always needed to have abstract, mathematical correctness -- think military, medical, industrial automation. I think those domains has more stringent requirement and a more focused usage, making the classes of inout narrower. A lot of software for B2B and B2C tries to be a kitchen sink and in the result get turned into a ball of mud. Some stuff should just be separate software. |
|
|
| ▲ | ekidd 3 hours ago | parent | prev | next [-] |
| There is a wide range of software that exists in a "adversarial" environment, including anything facing a network or processing outside data. At a minimum, this software should should not allow an attacker to execute code of their choice on a system handling private data. This does not require proving systems complete correct, but it does involve proving many properties of these systems. |
|
| ▲ | fsloth 2 hours ago | parent | prev | next [-] |
| You can combine both sometimes in application logic. Some API:s can be perfect. But then the real world adaptation needs to happen inside the module serving the API. |
|
| ▲ | turbobutton 3 hours ago | parent | prev | next [-] |
| Having been downvoted, I like to clarify that this comes from the experience working in finance with developers with a strong academic background that emphasized on the necessity of formal proof to a point where complexity made actual progress nearly impossible- while simultaneously basing the proof repeatedly on assumptions that did not uphold in practice. |
| |
| ▲ | i_am_a_peasant 3 hours ago | parent | next [-] | | Nah I don't disagree with you. Thing is even if you formally prove that for every input you produce a valid output. In safety certified software, there's the problem that if that input comes from a sensor, a sensor is an inherently probabilistic thing, and it may be that you will have false positives. The best you can do is build a safety case that even if you get false positives you end up in a safe state, but you can't guarantee that they won't ever increase operational costs. | | |
| ▲ | bajard 2 hours ago | parent [-] | | I once had a sensor that rounded the data, so the output unwittingly fitted into a grid. The equations that had to be used on that data gave infinite results because the grid sometimes rounded slopes into vertical lines. So I had to reconstruct a signal that fitted the data for the equations to work at all. But the reconstruction was no longer measured data. It was made up, and there was no single solution for fitting the data. That meant I could claim to "respect the data" while producing any result I wanted. | | |
| ▲ | i_am_a_peasant 2 hours ago | parent [-] | | Reminds me of that von Neumann quote "With four parameters I can fit an elephant, and with five I can make him wiggle his trunk." | | |
|
| |
| ▲ | perching_aix 3 hours ago | parent | prev [-] | | what were some categories of such assumptions, can you name some examples? a fun one that immediately comes to mind is asserting something holds for reals, but not evaluating whether it holds for IEEE floats, though maybe that's not really a thing in finance due to rounding related rules anyways |
|
|
| ▲ | bsenftner 2 hours ago | parent | prev [-] |
| [dead] |
