How to define and interpret natural language communication (and thus language) via protocols and state based parsing instead of just grammar.
3 Likes
P vs NP
2 Likes
I would like to see a push towards formal verification for software systems: a way to be able to take a software system and say āI can have assurance that this is correct, based on properties x, y, and zā. Using property based testing, strict type systems, and static analysis we can get a long way, but having a defined set of formal methods could provide us with a way to prove correctness in code similar to the way we can prove correctness in mathematics.
There are some really cool ideas surrounding Abstract Interpretation and Symbolic Execution that I would like to see make their way into development workflows. I really like the idea of being able to simulate how changes in one part of the system cascade to the rest. Being able to create snapshots of the entire system state at any given point in execution, for any given set of inputs, is such a cool concept and opens up the door for all kinds of in-depth analysis.
4 Likes
So, Idris?
Soā¦ LISP?
^.^
1 Like
Idris looks cool. There are a few others too, but they all seem to be on the fringes. I think at the moment there are still to many tradeoffs that come with these languages for most teams to justify using them. I donāt really know what it would take for people to pursue them though, it might be one of those things that we canāt really make easier and they will always remain a niche. Then again, plenty of people are choosing dynamically typed languages over typed alternatives that are just as easy to work with, so it could be that people just donāt care too much about these things regardless of how approachable they are.
I found this: an Idris to Erlang compiler. It looks like the idris compiler supports writing your own backend, similiar to ocaml, so it could potentially be used for āmission-criticalā
components in any language.
Iāll have to look more into lisp in the context of symbolic execution, though it makes sense that anything that has to do with parsing ast will be easier with lisp.
Iāve tried running that and although I can get basic things to compile, anything more complex and it just kind of keels over and dies, it needs more work. ^.^
But yes, Idris compiles to haskell by default.
LISP makes everything easier, until you really learn it you have no idea just how amazing it is. When it just āclicksā one day and you are suddenly like āUhh, lisp can do anything, and I donāt mean in a turing sense, I mean anything and everything that any other language can do or is doing now or in the future is possible to do in lisp in an even shorter and more readable wayā¦ Why is this not more popular?!?ā, then you read why it is not popular and realize that once upon a time it was, but it was so popular and so powerful in the AI community that when the AI community died it took LISP with it. ^.^;
If not for that, Iād easily say LISP would be one of the most used language forms out.
1 Like
Here are a few problems
- Store things forever (or until sun become red giant)
- Find Things
- Name Things
- Make secure systems
- Write correct code wrt some specifiction
- Reduce software complexity
- Reduce total amount of software
- Find way to employ or pay people made redundant by
fancy software - Stop people become zombies by distracting them all the time with trivia
- Use computation to optimize usage of limited resources
18 Likes
How far through the list are you Joe? 
There are a few things on your list I have thought about (hint: the less technically difficult ones 
)
Well, the last 3 of his list are more political/sociological than strictly computer science. Thoughts in those directions are interesting too, but Iām glad @joeerl took the thread back to its original question.
1 Like
Trueā¦ but computer science can have a profound effect on those things too 
Maybe we need another thread:
Which problems do you think can be solved with computers/technology?
I can see that getting really l o n g (because probably, most things can be solved with tech - given enough timeā¦)
1 Like
Explain to people why formal proof will just kill more people.
Creating a system that deals with errors, as all CS abstraction break in face of errors.
Kill the idea of Promises.
Take Time into account.
Propose high level languages or framework of thinking that deals with System Thinking and technique for engineering a safer world.
Teach the idea of Locality. (thanks actor modelā¦)
Yes i know they seems far different from everyone else, but they are the problem that create all the shit around us and the deep problems programming deal with.
1 Like
I think that IPFS might be making real progress in this area. Something I am enjoying playing around with for sure.
Universal basic income. Perhaps a software license on OSS that directs some profit from itās use to government/other orgs. Nice one to think about for sure.
I think this is a language problem. There are technical solutions to this but until the business owners can really discuss what the multiple actor timelines and simultaneity mean to there problem itās going to be hard to use them correctly
3 Likes
We need to build a Matrioshka Brain, a lot of our problems would then be solved, including āusā if we upload our minds to it and use earth as more raw materials to make more of the Matrioshka Brain. ^.^
Unique Human ID
Universal Basic Income
Universal Basic Land where you can plant a tree and build a house.
2 Likes
You can find list of unsolved problems in computer science in Wikipedia. Here is the link: https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_computer_science#Polynomial_versus_non-polynomial_time_for_specific_algorithmic_problems
1 Like
