欢迎大家赞助一杯啤酒🍺 我们准备了下酒菜:Formal mathematics/Isabelle/ML, Formal verification/Coq/ACL2, C++/F#/Lisp
灰狐咨询
小 (→简介) |
小 (→简介) |
||
第5行: | 第5行: | ||
灰狐服务:顾问、咨询、[[灰狐公开课|培训]]、支持 | 灰狐服务:顾问、咨询、[[灰狐公开课|培训]]、支持 | ||
+ | |||
+ | Formal semantics + [[Formal mathematics]] + [[Formal verification]] | ||
[[Open Provable Foundation]], 软硬件形式化验证教育培训和服务是核心咨询内容,[[ML]]/[[OCaml]]([[isabelle]]/HOL, [[Coq]]) & [[Haskell]]([[Agda]]) & [[Lisp]]([[ACL2]]) & [[C++]]([[Z3]])是核心语言和形式化能力。 | [[Open Provable Foundation]], 软硬件形式化验证教育培训和服务是核心咨询内容,[[ML]]/[[OCaml]]([[isabelle]]/HOL, [[Coq]]) & [[Haskell]]([[Agda]]) & [[Lisp]]([[ACL2]]) & [[C++]]([[Z3]])是核心语言和形式化能力。 | ||
第10行: | 第12行: | ||
编译器:[[GCC]], [[LLVM]] [[文件:GCC-logo.png]] [[文件:LLVM-logo.png]] | 编译器:[[GCC]], [[LLVM]] [[文件:GCC-logo.png]] [[文件:LLVM-logo.png]] | ||
− | + | 与合作伙伴一起策划和组建创新实验室。 | |
==目标== | ==目标== |
2023年5月3日 (三) 05:10的版本
灰狐咨询
目录 |
简介
灰狐,一个开放式组织,提供开源解决方案和咨询服务,你身边的开源顾问。
灰狐服务:顾问、咨询、培训、支持
Formal semantics + Formal mathematics + Formal verification
Open Provable Foundation, 软硬件形式化验证教育培训和服务是核心咨询内容,ML/OCaml(isabelle/HOL, Coq) & Haskell(Agda) & Lisp(ACL2) & C++(Z3)是核心语言和形式化能力。
与合作伙伴一起策划和组建创新实验室。
目标
致力于成为企业发展的长期合作伙伴。
帮助合作伙伴公司做好两件事:技术 + 增长(研发自动化、增长黑客)
咨询范围
提供开源解决方案和咨询服务,做你身边的开源顾问。
- 1、形式化验证、解决方案、订阅经济;
- 2、职业规划、职场建议、斜杠人生;
- 3、开源软件选型和支持服务;
- 4、编程语言和编译器虚拟机(核心领域)
- 5、金融、区块链、安全;
- 6、写作、自媒体、咨询师;
- 7、软件测试、研发管理、DevOps;
- 8、ERP、企业应用、电子商务运营;
- 9、认知科学、逻辑哲学和能力提升;
- 10、科学、技术、工程、数学(STEM)
相关内容
- DDD + Microservices 构建更成功的团队和软件
- 《精益创业》和《增长黑客》是启动和增长的基本框架,给出了新创企业的成长思维和最佳实践;
- 开放的企业文化、打造开放式组织,开源软件管理、企业开源、开源指南 开源项目服务 开放战略咨询;
- ActorX并发、异步、实时架构和基础设施咨询;
- IT管理/ITSM、IT基础设施架构、基础设施自动化、PaaS、CI/CD、DevOps、Google SRE运维实践;
- Debian/Ubuntu和Red Hat/CentOS Linux发行版、CoreOS/Atomic容器OS、机器人操作系统ROS、FreeRTOS/Zephyr微控制器实时操作系统、树莓派和Arduino、数据中心操作系统DC/OS、Redox A Rust operating system;
- Amazon Web Services、Microsoft Azure、Google Cloud Platform公有云咨询;
- 安全、防火墙、AWS 云安全性、身份与合规性 Google 安全模型
- Cassandra、PostgreSQL开源数据库替代Oracle、SQL Server商业数据库;
- 数据科学、大数据、人工智能、商业智能;
- 项目管理、研发管理;
- 开源软件企业内训,值得关注的开源软件推荐;
- 开源电商ERP/CRM/SCM/HR企业应用;
- 编译器、虚拟机、编程语言设计、Racket;
- 我们通过M3、E3、D3三个项目(简称MED)提供增长营销、企业应用、数据科学开源软件解决方案;
- 企业技术顾问、布道师。
服务项目
- 函数式编程:Haskell
- 编程模型:Actor model
- 数据模型
- 模块化:OSGi、Symfony
- 软件堆栈:SMACK stack
- 监控系统:Prometheus、Netdata
- 灰狐数据:D3、Anaconda、增长黑客
- 编程语言:C/C++/Rust/C#/PHP/Erlang程序设计,以Racket为设计实现平台讲解程序语言设计和编程语言原理。
- Android生态系统:Hack Android,围绕Android构建开放生态系统。
- 企业应用和电子商务:电商ERP和企业运营支撑系统。
- 区块链:全球金融的基础架构。
- 人工智能:数据挖掘、机器学习/深度学习
- 数据库:PostgreSQL、Apache HBase、Apache Cassandra
- 云存储:基于Ceph构建经济的PB/EB级的存储基础设施,是OpenStack等云平台的首选软件定义存储解决方案
- 私有云/PaaS:基于Rancher或Apache Mesos/DCOS + Kubernetes构建企业私有云、容器云。
软件供应链
开放供应链,确保开放源码的交付具有可信和一致的合规信息。
OpenChain Building Trust In The Supply Chain Since 2016
实施 Software Bill of Materials (SBOM) 标准,降低软件供应链风险。
- OWASP CycloneDX
- SPDX
- Dependency-Track Community Integrations
- Sonatype OSS INDEX Find Safe Components
- Open Source Software Supply Chain Best Practices at the Eclipse Foundation
TLS/SSL
SMACK堆栈
SMACK堆栈:基于 Spark, Mesos, Akka, Cassandra 和 Kafka 构建,The SMACK Stack is the New LAMP Stack
- Model: Scala and Akka
- Engine: Apache Spark
- Storage: Apache Cassandra
- Broker: Apache Kafka
- Manager: Apache Mesos
堆栈扩展
- 语言:Java、Kotlin、Scala、Clojure
- 框架:Apache OpenWhisk、Vert.x、Spring Boot、Scalatra、Play framework、Lagom
- 计算:Apache Spark、Deeplearning4j,分布式内存计算系统、大数据处理、机器学习
- 模型:ActorX、Akka,并发、容错、事件基础设施
- 消息:Apache Kafka、RabbitMQ,分布式消息系统、实时流式处理平台
- 存储:Apache Cassandra,分布式数据库、运营型数据管理平台
- 容器云:Docker、Kubernetes、Apache Mesos,容器、集群管理、数据中心操作系统
生态系统
- Android ecosystem
- Haskell ecosystem
- OCaml ecosystem
- Lisp ecosystem
- C++ ecosystem
- Rust ecosystem
- Scala ecosystem
- Kotlin ecosystem
- Clojure ecosystem
- Java ecosystem
- Erlang ecosystem
- Node.js ecosystem
- .NET ecosystem
- Akka ecosystem
- Kafka ecosystem
- Spark ecosystem
文档
- 开源已成为企业核心竞争力
- Mesos,数据中心操作系统的核心
- SMACK Architectures: Building data processing platforms with Spark, Mesos, Akka, Cassandra and Kafka
- 红帽 OpenShift 的业务价值
- 平台即服务、DevOps和应用集成:加速交付应用新途径
图集
客户
- 琥珀亲子:基础架构、DevOps、私有云、Apache Mesos,已经迁移至 Kubernetes。
- 魔租:研发管理、软件架构、分布式协作、技术支持、增长黑客
- 苏打出行:苏打实验室创新项目 微软AirSim用户组成员 微软VA&NLU&Bot预研
- 艾体验AIUX:筹备技术部、技术部发展规划、GitHub项目开发运维 人员招募、前沿技术研究、设备和技术规范等。
- 创道夫产业通:区块链项目
- 点点科技:开放服务联盟
- 更多案例
方式
现场服务、在线支持、知识星球
我们通过知识星球的社区方式和客户持续、深度交流,社区里有很多的行业和技术专家,大家可就一些具体问题一起展开交流和深入探讨。
知识星球:灰狐的朋友们
咨询师
咨询师/布道师,布道之道,引领团队拥抱技术创新
链接
- 红帽咨询
- Udemy培训课程 Fast Data Processing Systems with SMACK stack
- 书籍 Fast Data Processing Systems with SMACK Stack
- Building Streaming And Fast Data Applications With Spark, Mesos, Akka, Cassandra And Kafka
- Using Spark, Kafka, Cassandra and Akka on Mesos for Real-Time Personalization
- How we design enterprise software
- DataArt: Technology Consulting & Solution Design
- Container Solutions
- Altkom Software & Consulting