4 ms·

I think we need to train people to write formal specifications before we're going to see machine learning techniques generating useful programs. Sure sometimes

I think we need to train people to write formal specifications before we're going to see machine learning techniques generating useful programs. Sure sometimes an LLM generates a correct program. And sometimes horoscopes predict the future. I will be impressed when we can write a precise and formally verifiable specification of a program and some other program can generate the code for us from that specification and prove the generated implementation is faithful to the specification. An active area of research here, code synthesis, is promising! It's still a long way off from generating whole programs from a specification. The search spaces are not small. And even using a language as precise as mathematics leaves a lot of search space and ambiguity. Where we're going today with LLM's trying to infer a program from an imprecise specification written in informal language is simply disappointing.

canes123456 4y ago
A precise and formally verified specification is WAY harder to write then the code for it
- deleted 4y ago
  [deleted]
- agentultra 4y ago
  Exactly. It seems like we prefer the easy way out. If we can't write a precise specification then we don't know exactly what we want the computer to do. And so all we can get are guesses. The software industry has gotten this far with very little help from the formal methods community... that's changing in recent years in certain spaces where errors are magnified by scale like cloud computing, etc. But instead of getting better at writing precise specifications we're going to continue to be bad at it and hope that an LLM can manage to infer the correct program. It might be millions of lines of code but hopefully it does some of the things we want most of the time. Update: To be clear, I'm not saying AI/ML programs cannot help us to write programs at all, just that the inputs need to be better if we're going to have any confidence that the programs it generates are any better than a horoscope.
  - canes123456 4y ago
    I don't really see your point. AI/ML can make programs the same way as humans, which is writing a program that seems right but it very wrong and keep iterating until it mostly works, most of the time.
- pyrolistical 4y ago
  We could prob get LLM to help
- noobker 4y ago
  A precise and formally verified specification is usually just referred to as "PROD".
ClassAndBurn 4y ago
I agree here. Formal models have to become easier to create through. Today's ecosystem requires advanced knowledge of system design and still coding abilities. To democratize model generation we need a more iterative and understandable way of defining intented execution. The problem is this devolves into just coding the damn thing pretty quickly.
- agentultra 4y ago
  For sure! I agree, it needs better languages, education, and tooling. It's not about making a hard problem harder; it's about making it more accessible and straight-forward to teach and use in day-to-day work. Being more clear and precise in our specifications would only benefit us and the AI/ML tool generating the code. We could lean more on the correctness built into the entire stack rather than having to proof-read a mess of inferred code, something we're terribly ill-equipped to do.
  - valenterry 4y ago
    > Being more clear and precise in our specifications would only benefit us and the AI/ML tool generating the code Good luck with that. We have those languages already. For example Idris. It's just that now you are essentially doing a lot of math. And, funnily, I never hear people saying "making [math] more accessible and straight-forward to teach and use in day-to-day work". I wonder why...
denton-scratch 4y ago
> I think we need to train people to write formal specifications I don't think that is really a matter of training. You have to start with people who can think clearly; if they can't think clearly, it's hopeless to expect them to produce formal specs. Very few people can think clearly about difficult subjects. Of course, you can train people to improve the clarity of their thinking. I think that should be the main purpose of an undergraduate degree. Writing a formal spec is analagous to writing a program; if you can't program, your program won't work. So writing a formal spec proves that you can think clearly; but if you can think clearly, you can write a program without first writing a formal spec.
- _flux 4y ago
  Writing a formal spec in itself is a way to introduce clarity to thinking, because when writing it the spec itself lends to asking more and more questions about the things you might not have thought of. More so if there are tools to check your formal spec. But formal spec can be in higher level than the implementation. For example, it could be describing pre- and postconditions without actually stating out how to go from precondition to postcondition. I have noticed programming languages don't tend to ask the writer the right questions in the same way e.g. TLA+ and TLC do.
  - valenterry 4y ago
    The spec is the hard part. Just look at how many people are complaining about languages that use a statically type system. I wonder how many business people will then not complain about writing clear specs for "AI software". :)
Kinrany 4y ago
The article is not about generating correct programs.
lpapez 4y ago
> I will be impressed when we can write a precise and formally verifiable specification of a program and some other program can generate the code for us from that specification and prove the generated implementation is faithful to the specification. I cannot do this, and neither can any of the people I have ever worked with. Yet despite that we all call ourselves programmers, create value and earn money by writing ill-specified, often buggy code. Why would a tool need to be formally verified to be considered impressive and/or useful?
- evrimoztamur 4y ago
  Our approach shouldn't be to give up striving for better programs, algorithms, and code. Despite our current inability (which I don't think is a failure of programmers but business decisions), we can nevertheless reject further opportunities for decline, in name of profits, right?
  - lpapez 4y ago
    That is not what I said. Of course we should strive for precision, corectness etc. but that does not mean that current and future imprecise methods of development do not hold any value. There is plenty of value to be gained from poorly written software which we will keep writing until we get magically verified ones.
- naasking 4y ago
  We don't write formally verified code because writing the code to pass the verification is annoying and hard. If we're only writing the formally verified spec and a program or AI generated the code, that's a bit easier, though it may have to get easier still before it becomes mainstream.
- agentultra 4y ago
  > I cannot do this You could if you wanted to. You're smart, inventive, and creative. There's nothing stopping you from learning. > Why would a tool need to be formally verified to be considered impressive and/or useful? Part of it depends on your perspective. If we assume that an LLM (or some future ML tool based on it) is capable of producing code with the same rate of errors as a trained, expert human could then it would seem the productivity gain is not having to write all of that code ourselves. We already tolerate a certain amount of errors in our software and the world has not collapsed. The JVM had an error in its binary search implementation that lasted for nearly a decade before anyone noticed. They noticed because the size of the arrays being used started getting big enough that their programs started failing in mysterious ways. OpenSSL had a vulnerability that sat unnoticed for more than a decade. The cost of errors is not zero but it is tolerated. However the problem of programming is that we think it's our ability to write code which is the problem that is slowing us down. My perspective is that we're not focusing on the problem: that it is hard to be precise and write programs that work, whole cloth, from their specifications without any errors. Using an LLM to generate more code has another problem: while humans are decent enough at writing code to solve our problems, even if our solutions are imperfect, we're far worse at reading code and understanding what it does and whether it is correct with regards to some specification (if there is one). Empirical studies of large-scale code review are very humbling. We can read maybe 200 SLOC every couple of errors and have a negligible impact on error rates in the software being produced. More than that and the effect disappears. So now we have LLM's producing code that we know will have errors in it. And we have no idea where the error is. It could be a trivial error we could tolerate. Or it could be another Bar Mitzvah CVE. Hard to say. Even Betrand Meyer missed an error in a single-line expression generated by ChatGPT. He's way smarter than me. I don't see how we'll be able to keep up. But if we tackled the problem of getting better at being more precise with our specifications, I could definitely see how having an AI-like system automate code generation being really useful. There are plenty of times when working on a formal proof where you want to say, "this is obvious!," that have a machine verify that for you using the same proof rules and tactics you would use. Bonus points if it can explain the proof back to you. I just think we're a long way off from being able to do that.
ansgri 4y ago
We need to train people to write specifications since they seem to be the best way to fine-tune the AI performance for the task without changing the enormous dataset. Reinforcement learning methods can be used to tune the model in production under pressure of failing tests (executable specifications). Writing specifications to evaluate outcomes should be a better use of domain experts time than dataset cleaning. As for formality, real formal specifications are very hard, and LLMs are close to understanding natural language anyway, and 1000s of 90%-strict specs are better than 10 provably correct ones. So, some sort of legalese for machines will evolve.

canes123456 4y ago

A precise and formally verified specification is WAY harder to write then the code for it

deleted 4y ago
[deleted]
agentultra 4y ago
Exactly. It seems like we prefer the easy way out. If we can't write a precise specification then we don't know exactly what we want the computer to do. And so all we can get are guesses. The software industry has gotten this far with very little help from the formal methods community... that's changing in recent years in certain spaces where errors are magnified by scale like cloud computing, etc. But instead of getting better at writing precise specifications we're going to continue to be bad at it and hope that an LLM can manage to infer the correct program. It might be millions of lines of code but hopefully it does some of the things we want most of the time. Update: To be clear, I'm not saying AI/ML programs cannot help us to write programs at all, just that the inputs need to be better if we're going to have any confidence that the programs it generates are any better than a horoscope.
- canes123456 4y ago
  I don't really see your point. AI/ML can make programs the same way as humans, which is writing a program that seems right but it very wrong and keep iterating until it mostly works, most of the time.
pyrolistical 4y ago
We could prob get LLM to help
noobker 4y ago
A precise and formally verified specification is usually just referred to as "PROD".

ClassAndBurn 4y ago

I agree here. Formal models have to become easier to create through. Today's ecosystem requires advanced knowledge of system design and still coding abilities. To democratize model generation we need a more iterative and understandable way of defining intented execution. The problem is this devolves into just coding the damn thing pretty quickly.

agentultra 4y ago
For sure! I agree, it needs better languages, education, and tooling. It's not about making a hard problem harder; it's about making it more accessible and straight-forward to teach and use in day-to-day work. Being more clear and precise in our specifications would only benefit us and the AI/ML tool generating the code. We could lean more on the correctness built into the entire stack rather than having to proof-read a mess of inferred code, something we're terribly ill-equipped to do.
- valenterry 4y ago
  > Being more clear and precise in our specifications would only benefit us and the AI/ML tool generating the code Good luck with that. We have those languages already. For example Idris. It's just that now you are essentially doing a lot of math. And, funnily, I never hear people saying "making [math] more accessible and straight-forward to teach and use in day-to-day work". I wonder why...

denton-scratch 4y ago

> I think we need to train people to write formal specifications I don't think that is really a matter of training. You have to start with people who can think clearly; if they can't think clearly, it's hopeless to expect them to produce formal specs. Very few people can think clearly about difficult subjects. Of course, you can train people to improve the clarity of their thinking. I think that should be the main purpose of an undergraduate degree. Writing a formal spec is analagous to writing a program; if you can't program, your program won't work. So writing a formal spec proves that you can think clearly; but if you can think clearly, you can write a program without first writing a formal spec.

_flux 4y ago
Writing a formal spec in itself is a way to introduce clarity to thinking, because when writing it the spec itself lends to asking more and more questions about the things you might not have thought of. More so if there are tools to check your formal spec. But formal spec can be in higher level than the implementation. For example, it could be describing pre- and postconditions without actually stating out how to go from precondition to postcondition. I have noticed programming languages don't tend to ask the writer the right questions in the same way e.g. TLA+ and TLC do.
- valenterry 4y ago
  The spec is the hard part. Just look at how many people are complaining about languages that use a statically type system. I wonder how many business people will then not complain about writing clear specs for "AI software". :)

Kinrany 4y ago

The article is not about generating correct programs.

lpapez 4y ago

> I will be impressed when we can write a precise and formally verifiable specification of a program and some other program can generate the code for us from that specification and prove the generated implementation is faithful to the specification. I cannot do this, and neither can any of the people I have ever worked with. Yet despite that we all call ourselves programmers, create value and earn money by writing ill-specified, often buggy code. Why would a tool need to be formally verified to be considered impressive and/or useful?

evrimoztamur 4y ago
Our approach shouldn't be to give up striving for better programs, algorithms, and code. Despite our current inability (which I don't think is a failure of programmers but business decisions), we can nevertheless reject further opportunities for decline, in name of profits, right?
- lpapez 4y ago
  That is not what I said. Of course we should strive for precision, corectness etc. but that does not mean that current and future imprecise methods of development do not hold any value. There is plenty of value to be gained from poorly written software which we will keep writing until we get magically verified ones.
naasking 4y ago
We don't write formally verified code because writing the code to pass the verification is annoying and hard. If we're only writing the formally verified spec and a program or AI generated the code, that's a bit easier, though it may have to get easier still before it becomes mainstream.
agentultra 4y ago
> I cannot do this You could if you wanted to. You're smart, inventive, and creative. There's nothing stopping you from learning. > Why would a tool need to be formally verified to be considered impressive and/or useful? Part of it depends on your perspective. If we assume that an LLM (or some future ML tool based on it) is capable of producing code with the same rate of errors as a trained, expert human could then it would seem the productivity gain is not having to write all of that code ourselves. We already tolerate a certain amount of errors in our software and the world has not collapsed. The JVM had an error in its binary search implementation that lasted for nearly a decade before anyone noticed. They noticed because the size of the arrays being used started getting big enough that their programs started failing in mysterious ways. OpenSSL had a vulnerability that sat unnoticed for more than a decade. The cost of errors is not zero but it is tolerated. However the problem of programming is that we think it's our ability to write code which is the problem that is slowing us down. My perspective is that we're not focusing on the problem: that it is hard to be precise and write programs that work, whole cloth, from their specifications without any errors. Using an LLM to generate more code has another problem: while humans are decent enough at writing code to solve our problems, even if our solutions are imperfect, we're far worse at reading code and understanding what it does and whether it is correct with regards to some specification (if there is one). Empirical studies of large-scale code review are very humbling. We can read maybe 200 SLOC every couple of errors and have a negligible impact on error rates in the software being produced. More than that and the effect disappears. So now we have LLM's producing code that we know will have errors in it. And we have no idea where the error is. It could be a trivial error we could tolerate. Or it could be another Bar Mitzvah CVE. Hard to say. Even Betrand Meyer missed an error in a single-line expression generated by ChatGPT. He's way smarter than me. I don't see how we'll be able to keep up. But if we tackled the problem of getting better at being more precise with our specifications, I could definitely see how having an AI-like system automate code generation being really useful. There are plenty of times when working on a formal proof where you want to say, "this is obvious!," that have a machine verify that for you using the same proof rules and tactics you would use. Bonus points if it can explain the proof back to you. I just think we're a long way off from being able to do that.

ansgri 4y ago

We need to train people to write specifications since they seem to be the best way to fine-tune the AI performance for the task without changing the enormous dataset. Reinforcement learning methods can be used to tune the model in production under pressure of failing tests (executable specifications). Writing specifications to evaluate outcomes should be a better use of domain experts time than dataset cleaning. As for formality, real formal specifications are very hard, and LLMs are close to understanding natural language anyway, and 1000s of 90%-strict specs are better than 10 provably correct ones. So, some sort of legalese for machines will evolve.