[Agda] adapting Agda for next-gen blockchain apps

[Andreas Abel]

Hi Ren,

thanks for your message.  Unfortunately, I am not a crypto expert, so I 
cannot comment much on your requirements.

However, Agda is a general-purpose programming and verification 
language.  So I wonder which language features you are missing 
concretely for your project.  (Why) cannot you provide your special 
cryptographic functionality via a library?

Best regards,
Andreas

On 15.06.2016 13:23, Ren Rise wrote:
> Hi All,
> I am a Bitcoin enthusiast based in India. I am presently working on
> creating a decidable programming language codenamed XK for open source
> free programming on a new blockchain that does not necessarily require a
> positive cryptocurrency balance or computing fuel reserve unlike
> Ethereum. Our proposed blockchain will power next generation
> decentralized autonomous apps and organizations including blockchain
> banks, hedge funds, prime brokers, stock exchanges, forex dealers,
> automated software companies/factories and so on. This will empower new
> entrepreneurs, investors and others those who feel disadvantaged
> vis-à-vis big institutional investors and MNCs.
> We envision XK to support following four categories of applications and
> functions primarily:
>
>  1. Decentralized trustless financial Contracts (without any need for
>     3^rd party custodians like banks and stock exchanges): This list
>     includes equity, forex, commodity and event derivatives e.g.
>     options, functions, swaps, swaptions, cryptostocks, cryptobonds and
>     so on.
>  2. Time-aware Self-organizing autonomous systems. This list includes
>     automated trading systems and strategy engines, realtime voice
>     agents like SIRI and realtime activity supervisors and enforcer bots.
>  3. Autonomic Dispute Resolution, Blockchain Law/Code Interpretation &
>     Arbitration
>  4. Automated software testing, debugging, verification and license
>     distribution as well as tracking.
>
> I was thinking of extracting the selected features of Intuitionistic
> Ancestral Logic with dependent types, Intuitionistic Logic that proves
> Markov’s Principle as well as of Algebraic topology-based self-learning,
> self-planning and self-executing distributed computing domain Phase Web
> introduced by Michael Manthey. Phase Web has got connection with both
> Chu automaton and growing Petrinets (growing in both nodes and
> connections to reflect complexity, learning, planning etc.).
> How do we adapt your Adga for our purpose? Would it be feasible for us
> to add desired higher-order capabilities to Agda for our target apps? If
> yes, what would be the ideal development path and roadmap?
> I look forward to hearing from you.
> Best regards,
> Ren Aryan
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/