4 ms·

I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that wo

I agree. I said first-order logic because I think it is more accessible. Coq, Agda, Idris, etc. employ I think some pretty sophisticated type theory and that would all have to be packaged up in a way that is accessible to an average programmer.

wyager 10y ago
> in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.
- dkarapetyan 10y ago
  I don't think accessibility is a bad thing. I think computing, its practice and theory, should be taught the same way we teach literacy. I didn't mean "average" as in "incompetent". If writing contracts was as simple as writing a few lines of code in some formal language that didn't require a law or finance degree then I would consider that to be a good thing. It would be even better if the system was designed from first principles with solid theory backing it.
  - wyager 10y ago
    I totally agree, but the reality is that in order to write contracts that are sure to be correct, you need a level of expertise that involves much more work than just learning how to write programs. Knowing the syntax and usage of a rigorously-typed language like Agda is the easy part.
    - kowdermeister 10y ago
      Then the platform is flawed. Average programmers should be able to understand it easily. It's not that hard, some wants X and some wants Y in exchange. I'm not a lawyer but I write contracts with my clients. If you keep things simple it should fit most people. making g smart contracts complicated you keep it in the area of a small elite who are knowledgeable of playing safe with it. I wold go as far as make it as simple as HTML.
      - wyager 10y ago
        That's what standardized contracts are for. Tellers don't write the legalese on your credit card receipt. They just print it out.
- Paradigma11 10y ago
  But : https://en.wikipedia.org/wiki/Solidity https://en.wikipedia.org/wiki/Solidity "As specified by Wood it is designed around the ECMAScript syntax to make it familiar for existing web developers;"

wyager 10y ago

> in a way that is accessible to an average programmer. The average programmer should not be writing multi-million-dollar contracts.

dkarapetyan 10y ago
I don't think accessibility is a bad thing. I think computing, its practice and theory, should be taught the same way we teach literacy. I didn't mean "average" as in "incompetent". If writing contracts was as simple as writing a few lines of code in some formal language that didn't require a law or finance degree then I would consider that to be a good thing. It would be even better if the system was designed from first principles with solid theory backing it.
- wyager 10y ago
  I totally agree, but the reality is that in order to write contracts that are sure to be correct, you need a level of expertise that involves much more work than just learning how to write programs. Knowing the syntax and usage of a rigorously-typed language like Agda is the easy part.
  - kowdermeister 10y ago
    Then the platform is flawed. Average programmers should be able to understand it easily. It's not that hard, some wants X and some wants Y in exchange. I'm not a lawyer but I write contracts with my clients. If you keep things simple it should fit most people. making g smart contracts complicated you keep it in the area of a small elite who are knowledgeable of playing safe with it. I wold go as far as make it as simple as HTML.
    - wyager 10y ago
      That's what standardized contracts are for. Tellers don't write the legalese on your credit card receipt. They just print it out.
Paradigma11 10y ago
But : https://en.wikipedia.org/wiki/Solidity https://en.wikipedia.org/wiki/Solidity "As specified by Wood it is designed around the ECMAScript syntax to make it familiar for existing web developers;"