3 ms·

I'm so glad the industry starts adopting formal proofs more and more... After 20 years in the industry i still feel like a caveman, coding as best as i can, hop

by bsaul 2y ago

I'm so glad the industry starts adopting formal proofs more and more... After 20 years in the industry i still feel like a caveman, coding as best as i can, hoping nothing bad will happen (and then sighing at the sight of the 100ks line counts of my project). Maybe having more powerful code generators like LLMs will shift us toward spending more time on specification and modelling ? Let's hope so.

canadianfella 2y ago
[dead]
diggan 2y ago
Some (balanced) automated testing gets you away from "hoping nothing bad will happen" while not having to spend a year coming up with a formal proof for your program. Worth testing if you haven't ;)
- bsaul 2y ago
  of course, i do test. But let's be honest, if the person writing the tests is the same as the one writing the code, chances are the tests won't discover flaws in the model of the original design.
  - sanxiyn 2y ago
    Try property testing. Property tests written by myself routinely discover bugs in my codes.
  - dllthomas 2y ago
    I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you think to test for. It's not clear to me that it's meaningfully stronger than the correlation with things you forget to prove. Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.
- Aerbil313 2y ago
  Contrary opinion: Writing your program is much easier once you write the proof, because you basically formulate your entire program.
wongarsu 2y ago
In the last decade or so there has been an explosion in the popularity of explicitly typed languages. Typescript, typed python, Rust with its very strict and expressive type system, etc. That's not full formal proofs of the entire behavior, but it's a solid step back in that direction. Imho any change in this direction is predicated on tooling and developer experience. Explicit typing was made easier by smarter autocomplete from better IDE plugins, and those same plugins make more valuable suggestions if you have better types, creating a virtuous circle. Nothing of the form exists so far for formal proofs. If you limit it to small sections of behavior it might pass as a smart but obscure way to write unit tests (ensuring that certain behaviors hold). But nothing outside of your unit tests benefits from it. Maybe making the specification the starting point from which an LLM writes code changes that. But so far all the evidence points to people being very bad at writing specifications and preferring imperative over declarative languages.
- AceJohnny2 2y ago
  > Rust with its very strict and expressive type system Tangentially, I find it very interesting how Rust could have had fully inferred types (like OCaml does), but chose to require specifying types at function boundaries. It shows a thoughtful balance of what the system can technically do, and what's actually useful to the humans dealing with the code.
- RandomThoughts3 2y ago
  Rust doesn’t have a very expressive type system. Rust type system would have been at home twenty years ago. Ocaml already had a better type system when I used it professionally in the 2010s and they have added a lot since and you could already type infer everything. I’m sorry but implying that having typing becoming a bit more popular is a significant step towards formal proof is akin to saying we are getting closer to using efficient heating because we have switched from burning peat to coal.
pjmlp 2y ago
If more languages adopted Design by Contract, and the capabilities for Type Driven Development, we would already be much better, without formal methods, many of which aren't supported in common languages and there is always something lost in translation.
- RandomThoughts3 2y ago
  > there is always something lost in translation. SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other ADA code. Sorry but implying that the issue is things “lost in translation” is a complete cope out. I’m very sour about the disdain for formal proof in the field. I understand the wish to iterate fast for user-facing elements but the fact that we use the same development techniques for the backbone of our infrastructure is nothing short of insane from my point of view. There is a self defeating attitude with regard to formal tool which is that they are too costly and too complicated to use outside of things for which they are mandatory. It means people are not trained in how to use them so it’s hard and costly to find someone who will prove your code and this vicious cycle somehow feeds itself.
  - pjmlp 2y ago
    My "lost in translation" remark naturally doesn't apply to SPARK, rather to stuff like TLA+ that don't have any mapping to actual programming languages, unlike stuff like Ada/Spark, Frama-C or even Design by Contract. It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings, without any relation between the mathematical model and the C implementation.
    - superidiot1932 2y ago
      >It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings Bold statement, at least in that case you know the algorithm isn't wrong.

by bsaul 2y ago

canadianfella 2y ago

[dead]

diggan 2y ago

Some (balanced) automated testing gets you away from "hoping nothing bad will happen" while not having to spend a year coming up with a formal proof for your program. Worth testing if you haven't ;)

bsaul 2y ago
of course, i do test. But let's be honest, if the person writing the tests is the same as the one writing the code, chances are the tests won't discover flaws in the model of the original design.
- sanxiyn 2y ago
  Try property testing. Property tests written by myself routinely discover bugs in my codes.
- dllthomas 2y ago
  I think there's definitely something to the notion that there will be correlation between things you forget to (try to) guarantee in your code and things you think to test for. It's not clear to me that it's meaningfully stronger than the correlation with things you forget to prove. Any which way, more prodding of the model (mental or more formal) is probably going to help correctness but may or may not be worth the cost, depending.
Aerbil313 2y ago
Contrary opinion: Writing your program is much easier once you write the proof, because you basically formulate your entire program.

wongarsu 2y ago

In the last decade or so there has been an explosion in the popularity of explicitly typed languages. Typescript, typed python, Rust with its very strict and expressive type system, etc. That's not full formal proofs of the entire behavior, but it's a solid step back in that direction. Imho any change in this direction is predicated on tooling and developer experience. Explicit typing was made easier by smarter autocomplete from better IDE plugins, and those same plugins make more valuable suggestions if you have better types, creating a virtuous circle. Nothing of the form exists so far for formal proofs. If you limit it to small sections of behavior it might pass as a smart but obscure way to write unit tests (ensuring that certain behaviors hold). But nothing outside of your unit tests benefits from it. Maybe making the specification the starting point from which an LLM writes code changes that. But so far all the evidence points to people being very bad at writing specifications and preferring imperative over declarative languages.

AceJohnny2 2y ago
> Rust with its very strict and expressive type system Tangentially, I find it very interesting how Rust could have had fully inferred types (like OCaml does), but chose to require specifying types at function boundaries. It shows a thoughtful balance of what the system can technically do, and what's actually useful to the humans dealing with the code.
RandomThoughts3 2y ago
Rust doesn’t have a very expressive type system. Rust type system would have been at home twenty years ago. Ocaml already had a better type system when I used it professionally in the 2010s and they have added a lot since and you could already type infer everything. I’m sorry but implying that having typing becoming a bit more popular is a significant step towards formal proof is akin to saying we are getting closer to using efficient heating because we have switched from burning peat to coal.

pjmlp 2y ago

If more languages adopted Design by Contract, and the capabilities for Type Driven Development, we would already be much better, without formal methods, many of which aren't supported in common languages and there is always something lost in translation.

RandomThoughts3 2y ago
> there is always something lost in translation. SPARK is more than 20 years old at that point and allows you to easily use formally proven code next to other ADA code. Sorry but implying that the issue is things “lost in translation” is a complete cope out. I’m very sour about the disdain for formal proof in the field. I understand the wish to iterate fast for user-facing elements but the fact that we use the same development techniques for the backbone of our infrastructure is nothing short of insane from my point of view. There is a self defeating attitude with regard to formal tool which is that they are too costly and too complicated to use outside of things for which they are mandatory. It means people are not trained in how to use them so it’s hard and costly to find someone who will prove your code and this vicious cycle somehow feeds itself.
- pjmlp 2y ago
  My "lost in translation" remark naturally doesn't apply to SPARK, rather to stuff like TLA+ that don't have any mapping to actual programming languages, unlike stuff like Ada/Spark, Frama-C or even Design by Contract. It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings, without any relation between the mathematical model and the C implementation.
  - superidiot1932 2y ago
    >It is meaningless to model a great algorithm in abstract mathematical models, and then let someone else implementing them in C89 with raw BSD sockets and C strings Bold statement, at least in that case you know the algorithm isn't wrong.