cads: mircea_popescu: *shrug* I do this when I make a connection that turns a deep problem into a resource. You should have seen me years ago each time I realized some little math connection.

cads: mircea_popescu: when you realize that this approach takes Coq -> Haskell -> C code, then you see it's about putting Coq in Cunt. Simple. I know ten medium level programmers already dying to be doing this kind of work, even if it was near free.

cads: Can I hear "verified"?

cads: I might see some champing at the bit :)

cads: mircea_popescu: thanks for that stimulating line of thought, I'm getting some positive feedback from my peers already.

cads: also, I know any number of people that play with the technology _for fun_, but much fewer who have names for themselves (and those guys tend to be happily employed)

cads: The issue I see with formal verification is so few people know to ask for it by name

cads: and I mean employees

cads: I'm thinking risk and externalities on the insurance derivative over this kind of service would be _far_ beyond my abilities to manage. However a code review would be quite lucrative and low risk. Also, it might be reasonable to begin offering formal verification services from the gate, or about 1 year after startup. It's not that hard to teach. When you have your own slaves.

cads: I think I might have hit on an interesting idea

cads: plenty of time to play in that regard when I am entirely more possessed of my own sense of greatness

cads: mircea_popescu: very dark. That always seems like nothing more than a game to me. I think I'd have to develop the ownership mentality to be a really good master.

cads: mircea_popescu: ah, those kinds of slave. And they have so much to learn I can understand why teaching anyone else might be low priority.

cads: and that's where I find the real breakthroughs happen

cads: well to give an example I helped a friend for free to learn inequalities. Helped me breakthrough a new way to teach inequalities. Spent a couple hours. On the other hand, I charge so much for tutoring that my students often can't afford two hour stretches.

cads: something I ought to change.

cads: mircea_popescu: I tend to give my best advice without knowing it to friends, lol. And less good advice to my consutancy.

cads: I have no problem refactoring the code to scale it

cads: I am also recruiting investors for a 3d printing business I'd like to help my brother set up

cads: but I should certainly be able to push up a _small_ service

cads: I might be overcommitting

cads: but I also have work in applied logic and economics and game theory that is promising

cads: if I do, then yes, I expect to use topics like this for my masters/phd

cads: pgp: I'm not sure if I'm going to remain in school

cads: Okay, I will first brainstorm about a ~10BTC service

cads: yeah, I also believe offering provability services would be a great extension to that model

cads: But yes. That is the type of sector I wish to enter.

cads: mircea_popescu: though I would be thrilled to offer that, frankly I would need 5 years of software dev manager work before I could assemble and run such a team, to completely forget about capital.

cads: very well, I am optimistic about this response

cads: I think that would be a suitable initial offering.

cads: of course, whether I give my income to charity will be a private decision then. My inventive to serve the project honestly will come from that.

cads: If I have to set myself up to financially benefit, and hold the new company as a private organization, I will

cads: I can see reason.

cads: I am starting to change my opinion, due to the 'trust' argument

cads: mircea_popescu: I have already been advised once that for the project to succeed and be safe and beneficial long term.

cads: I agree

cads: I do not wish to profit from it in ways other than 1) public reputation if I succed, and 2) transferrable skills regardless of whether I fail or succeed.

cads: I believe I am creating this exchange as a gift to the community

cads: I do not wish to profit from recieving your public endorsement, no.

cads: mircea_popescu: I would certainly keep you on the anonymous gratitude lisk

cads: mircea_popescu: I believe that what a student can do greatly increases even by having a teacher that says 'it is possible'. Moral support means philosophical and encouragement. It would mean a great deal to have whatever positive, constructive input you wish to provide. When we provide others with moral support, we do it only so far as it helps our reputation or internal sense of gratification at having helped someone.

cads: Also, as I intend to publicly document each step of the process, and then release the result for free to whoever wishes to provide starting reserve capital, I understand I will get ridiculed

cads: MJR, I will be following the classical "Composing Contracts" paper: http://contracts.scheming.org/

cads: eventually when I can model arbitrary contracts, they will be implemented as a non-turing complete contract-composition syntax

cads: in fact, I think I'm happy with your proposed offering of whatever I can pick up in here.

cads: This is all. I do not expect more than an hour each week of interspersed conversation. About as much as we've talked already, in fact.

cads: mircea_popescu: aside from moral support and guidance, I will ask questions about how the mpex was implemented.

cads: mircea_popescu: I am a mathematician, not a coder, so I don't expect this project to succeed without some serious help. I have the whole #haskell community. I have 5 years of haskell. I can use ruby, python, php etc for frontend. I will rework my ideas on attribution and profit share (it may be best to arrange that I profit financially from a successful completion). Will this be a project you can provide moral support to?

cads: and yes, I said Coq :P

cads: Scrat: I agree writing the code in haskell would make the software obscure. However I know a number of derivatives design and valuation packages that run in haskell. Haskell has great support for financial contracts.

cads: "free work", of course, is not work I do for free, but work I do to increase my public reputation in ways beyond what normal allowances of authority would give.

cads: mircea_popescu: this is part of what I consider my "free work". Some people do a finance internship. I will build an exchange.

cads: I in turn have some wonky ideas. I want to build the core engine in haskell. I want to release the software for free. I'd like to help run the exchange, but I do not wish to be paid for it.

cads: I agree. I would be asking essentially for 'gratis' financial consulting. Not a winning proposition for you by any means.

cads: mircea_popescu: barring any formal mentorship/student relationship, I would like at least to ask you basic questions over the next few months.

cads: mircea_popescu: I would not be able to pay you for your time. I would want to talk to you about high level architecture and implementation details.